{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE TypeFamilies #-}

module Agda.TypeChecking.Primitive.Cubical
  ( module Agda.TypeChecking.Primitive.Cubical
  , module Agda.TypeChecking.Primitive.Cubical.Id
  , module Agda.TypeChecking.Primitive.Cubical.Base
  , module Agda.TypeChecking.Primitive.Cubical.Glue
  , module Agda.TypeChecking.Primitive.Cubical.HCompU
  )
  where

import Prelude hiding (null, (!!))

import Control.Monad
import Control.Monad.Except
import Control.Monad.Trans ( lift )
import Control.Exception

import Data.String

import Data.Bifunctor ( second )
import Data.Either ( partitionEithers )
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import Data.Foldable hiding (null)

import Agda.Interaction.Options ( optCubical )

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern

import Agda.TypeChecking.Names
import Agda.TypeChecking.Primitive.Base
import Agda.TypeChecking.Monad

import Agda.TypeChecking.Free
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Telescope

import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Maybe

import Agda.Utils.Impossible
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Tuple
import Agda.Utils.Size
import Agda.Utils.BoolSet (BoolSet)
import qualified Agda.Utils.Pretty as P
import qualified Agda.Utils.BoolSet as BoolSet

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

primPOr :: TCM PrimitiveImpl
primPOr :: TCM PrimitiveImpl
primPOr = do
  Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
  Type
t    <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel)    forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a  ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i  ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"j" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
j  ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT (TCMT IO) Term
i NamesT (TCMT IO) Term
j) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
o -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
          ((forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"i1" NamesT (TCMT IO) Term
i forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i1 -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a forall a b. (a -> b) -> a -> b
$ NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne1 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
j forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i1))) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
          ((forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"j1" NamesT (TCMT IO) Term
j forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
j1 -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a forall a b. (a -> b) -> a -> b
$ NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne2 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
j forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
j1))) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
          forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT (TCMT IO) Term
i NamesT (TCMT IO) Term
j) (\ NamesT (TCMT IO) Term
o -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a forall a b. (a -> b) -> a -> b
$ NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Nat
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Nat
6 forall a b. (a -> b) -> a -> b
$ \ [Arg Term]
ts -> do
    case [Arg Term]
ts of
     [Arg Term
l,Arg Term
i,Arg Term
j,Arg Term
a,Arg Term
u,Arg Term
v] -> do
       Blocked (Arg Term)
si <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
i
       IntervalView
vi <- forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
si
       case IntervalView
vi of
        IntervalView
IOne -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn (forall e. Arg e -> e
unArg Arg Term
u)
        IntervalView
IZero -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn (forall e. Arg e -> e
unArg Arg Term
v)
        IntervalView
_ -> do
          Blocked (Arg Term)
sj <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
j
          IntervalView
vj <- forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sj
          case IntervalView
vj of
            IntervalView
IOne -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn (forall e. Arg e -> e
unArg Arg Term
v)
            IntervalView
IZero -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn (forall e. Arg e -> e
unArg Arg Term
u)
            IntervalView
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction [forall a. a -> MaybeReduced a
notReduced Arg Term
l,Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
si,Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sj,forall a. a -> MaybeReduced a
notReduced Arg Term
a,forall a. a -> MaybeReduced a
notReduced Arg Term
u,forall a. a -> MaybeReduced a
notReduced Arg Term
v]


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

primPartial' :: TCM PrimitiveImpl
primPartial' :: TCM PrimitiveImpl
primPartial' = do
  Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
  Type
t <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
       forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (\ NamesT (TCMT IO) Term
a ->
        forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"φ" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ ->
        forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
        (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a))
  Term
isOne <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne
  Term
v <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"a" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
l ->
        forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"φ" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
        forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"A" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
        forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"p" NamesT (TCMT IO) Term
phi (\NamesT (TCMT IO) Term
_ -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
l NamesT (TCMT IO) Term
a)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Nat
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Nat
0 forall a b. (a -> b) -> a -> b
$ \ [Arg Term]
_ -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn Term
v

primPartialP' :: TCM PrimitiveImpl
primPartialP' :: TCM PrimitiveImpl
primPartialP' = do
  Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
  Type
t <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
       forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (\ NamesT (TCMT IO) Term
a ->
        forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"φ" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
        forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"A" (forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
phi forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
        (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a))
  Term
v <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"a" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
l ->
        forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"φ" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
        forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"A" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
        forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"p" NamesT (TCMT IO) Term
phi (\ NamesT (TCMT IO) Term
p -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
l (NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
p))
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Nat
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Nat
0 forall a b. (a -> b) -> a -> b
$ \ [Arg Term]
_ -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn Term
v

primSubOut' :: TCM PrimitiveImpl
primSubOut' :: TCM PrimitiveImpl
primSubOut' = do
  Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
  Type
t    <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"φ" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"u" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's NamesT (TCMT IO) Term
a forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPartial forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
u ->
          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's NamesT (TCMT IO) Term
a (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
u) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Nat
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Nat
5 forall a b. (a -> b) -> a -> b
$ \ [Arg Term]
ts -> do
    case [Arg Term]
ts of
      [Arg Term
a,Arg Term
bA,Arg Term
phi,Arg Term
u,Arg Term
x] -> do
        Term -> IntervalView
view <- forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
        Blocked (Arg Term)
sphi <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
        case Term -> IntervalView
view forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sphi of
          IntervalView
IOne -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall (m :: * -> *) a. Monad m => a -> m a
return (forall e. Arg e -> e
unArg Arg Term
u) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> (forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm [Char]
builtinSubOut [Char]
builtinItIsOne))
          IntervalView
_ -> do
            Blocked (Arg Term)
sx <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
x
            Maybe QName
mSubIn <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinSubIn
            case forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sx of
              Def QName
q [Elim
_,Elim
_,Elim
_, Apply Arg Term
t] | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mSubIn -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn (forall e. Arg e -> e
unArg Arg Term
t)
              Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
a,Arg Term
bA] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi, forall a. a -> MaybeReduced a
notReduced Arg Term
u, Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sx]
      [Arg Term]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

primTrans' :: TCM PrimitiveImpl
primTrans' :: TCM PrimitiveImpl
primTrans' = do
  Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
  Type
t    <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Functor m => m Term -> m Type
el (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"A" (forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i -> (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i))) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"φ" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
          (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) (NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne) (NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne))
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Nat
-> ([Arg Term] -> Nat -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
PrimFun forall a. HasCallStack => a
__IMPOSSIBLE__ Nat
4 forall a b. (a -> b) -> a -> b
$ \ [Arg Term]
ts Nat
nelims -> do
    Command
-> [Arg Term] -> Nat -> ReduceM (Reduced MaybeReducedArgs Term)
primTransHComp Command
DoTransp [Arg Term]
ts Nat
nelims

primHComp' :: TCM PrimitiveImpl
primHComp' :: TCM PrimitiveImpl
primHComp' = do
  Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
  Type
t    <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"φ" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType (\ NamesT (TCMT IO) Term
i -> forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
phi forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
          (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Nat
-> ([Arg Term] -> Nat -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
PrimFun forall a. HasCallStack => a
__IMPOSSIBLE__ Nat
5 forall a b. (a -> b) -> a -> b
$ \ [Arg Term]
ts Nat
nelims -> do
    Command
-> [Arg Term] -> Nat -> ReduceM (Reduced MaybeReducedArgs Term)
primTransHComp Command
DoHComp [Arg Term]
ts Nat
nelims

-- | Construct a helper for CCHM composition, with a string indicating
-- what function uses it.
mkComp :: HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)
mkComp :: forall (m :: * -> *).
HasBuiltins m =>
[Char]
-> NamesT
     m
     (NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term)
mkComp [Char]
s = do
  let getTermLocal :: [Char] -> NamesT m Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm [Char]
s
  Term
tIMax  <- [Char] -> NamesT m Term
getTermLocal [Char]
builtinIMax
  Term
tINeg  <- [Char] -> NamesT m Term
getTermLocal [Char]
builtinINeg
  Term
tHComp <- [Char] -> NamesT m Term
getTermLocal [Char]
builtinHComp
  Term
tTrans <- [Char] -> NamesT m Term
getTermLocal [Char]
builtinTrans
  Term
iz     <- [Char] -> NamesT m Term
getTermLocal [Char]
builtinIZero
  Term
io     <- [Char] -> NamesT m Term
getTermLocal [Char]
builtinIOne

  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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTrans
      forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" forall a b. (a -> b) -> a -> b
$ \NamesT m Term
i -> NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
i forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
`imax` NamesT m Term
r))
      forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" forall a b. (a -> b) -> a -> b
$ \NamesT m Term
i -> NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
i forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
`imax` NamesT m Term
r))
      forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
r
      forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u

  forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 ->
    forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
phi
                forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\NamesT m Term
i -> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" forall a b. (a -> b) -> a -> b
$ \NamesT m Term
o ->
                        NamesT m Term
-> NamesT m Term -> 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 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o))
                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 (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz) NamesT m Term
u0

-- | Construct an application of buitlinComp. Use instead of 'mkComp' if
-- reducing directly to hcomp + transport would be problematic.
mkCompLazy
  :: HasBuiltins m
  => String
  -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)
mkCompLazy :: forall (m :: * -> *).
HasBuiltins m =>
[Char]
-> NamesT
     m
     (NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term)
mkCompLazy [Char]
s = do
  let getTermLocal :: [Char] -> NamesT m Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm [Char]
s
  Term
tComp <- [Char] -> NamesT m Term
getTermLocal [Char]
builtinComp
  forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u0

-- | Implementation of Kan operations for Pi types. The implementation
-- of @transp@ and @hcomp@ for Pi types has many commonalities, so most
-- of it is shared between the two cases.
doPiKanOp
  :: KanOperation -- ^ Are we composing or transporting?
  -> ArgName      -- ^ Name of the binder
  -> FamilyOrNot (Dom Type, Abs Type)
  -- ^ The domain and codomain of the Pi type.
  -> ReduceM (Maybe Term)
doPiKanOp :: KanOperation
-> [Char]
-> FamilyOrNot (Dom' Term Type, Abs Type)
-> ReduceM (Maybe Term)
doPiKanOp KanOperation
cmd [Char]
t FamilyOrNot (Dom' Term Type, Abs Type)
ab = do
  let getTermLocal :: [Char] -> ReduceM Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm forall a b. (a -> b) -> a -> b
$ KanOperation -> [Char]
kanOpName KanOperation
cmd forall a. [a] -> [a] -> [a]
++ [Char]
" for function types"

  Term
tTrans <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinTrans
  Term
tHComp <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinHComp
  Term
tINeg <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinINeg
  Term
tIMax <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinIMax
  Term
iz    <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinIZero

  -- We must guarantee that the codomain is a fibrant type, i.e. one
  -- that supports hcomp and transp. Otherwise, what are we even doing!
  let
    toLevel' :: a -> m (Maybe (Level' Term))
toLevel' a
t = do
      Sort
s <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort a
t
      case Sort
s of
        Type Level' Term
l -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Level' Term
l)
        Sort
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    -- But this case is actually impossible:
    toLevel :: a -> f (Level' Term)
toLevel a
t = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {m :: * -> *} {a}.
(MonadReduce m, LensSort a) =>
a -> m (Maybe (Level' Term))
toLevel' a
t

  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall {m :: * -> *} {a}.
(MonadReduce m, LensSort a) =>
a -> m (Maybe (Level' Term))
toLevel' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst a => Abs a -> a
absBody forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FamilyOrNot a -> a
famThing forall a b. (a -> b) -> a -> b
$ FamilyOrNot (Dom' Term Type, Abs Type)
ab) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ Level' Term
_ -> do
  forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do

    -- When doing transport in Pi types, we need to distinguish a couple
    -- of different cases depending on the sort of the domain, since
    -- there are a couple of different possibilities for how we end up
    -- with a fibrant Pi type:
    Maybe
  ((NamesT ReduceM Term -> NamesT ReduceM Term)
   -> NamesT ReduceM Term
   -> NamesT ReduceM Term
   -> NamesT ReduceM Term)
trFibrantDomain <- do
      let
        (Dom' Term Type
x, Term -> Term
f) = case FamilyOrNot (Dom' Term Type, Abs Type)
ab of
          IsFam (Dom' Term Type
a, Abs Type
_) -> (Dom' Term Type
a, \ Term
a -> forall a. Names -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
a)))
          IsNot (Dom' Term Type
a, Abs Type
_) -> (Dom' Term Type
a, forall a. a -> a
id)
      Sort
s <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort Dom' Term Type
x
      case Sort
s of
        -- We're looking at a fibrant Pi with fibrant domain: Transport
        -- backwards along the domain.
        Type Level' Term
lx -> do
          [NamesT ReduceM Term
la, NamesT ReduceM Term
bA] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
f) [Level' Term -> Term
Level Level' Term
lx, forall t a. Type'' t a -> a
unEl forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom forall a b. (a -> b) -> a -> b
$ Dom' Term Type
x]
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ \NamesT ReduceM Term -> NamesT ReduceM Term
iOrNot NamesT ReduceM Term
phi NamesT ReduceM Term
a0 ->
            forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTrans forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"j" (\NamesT ReduceM Term
j -> NamesT ReduceM Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term -> NamesT ReduceM Term
iOrNot NamesT ReduceM Term
j)
              forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"j" (\ NamesT ReduceM Term
j -> NamesT ReduceM Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term -> NamesT ReduceM Term
iOrNot NamesT ReduceM Term
j)
              forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
phi
              forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
a0

        -- We're looking a fibrant Pi whose domain is a lock: No need to do anything.
        Sort
LockUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ \NamesT ReduceM Term -> NamesT ReduceM Term
_ NamesT ReduceM Term
_ NamesT ReduceM Term
a0 -> NamesT ReduceM Term
a0

        -- We're looking at an unmarked path type. Make sure that the
        -- domain is actually the interval before continuing without an
        -- adjustment, though!
        Sort
IntervalUniv -> do
          Blocked Type
x' <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom' Term Type
x
          Maybe QName
mInterval <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinInterval
          case forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked Type
x' of
            Def QName
q [] | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mInterval -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ \NamesT ReduceM Term -> NamesT ReduceM Term
_ NamesT ReduceM Term
_ NamesT ReduceM Term
a0 -> NamesT ReduceM Term
a0
            Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

        Sort
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

    forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe
  ((NamesT ReduceM Term -> NamesT ReduceM Term)
   -> NamesT ReduceM Term
   -> NamesT ReduceM Term
   -> NamesT ReduceM Term)
trFibrantDomain (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \(NamesT ReduceM Term -> NamesT ReduceM Term)
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
trA -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    [NamesT ReduceM Term
phi, NamesT ReduceM Term
u0] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [forall t a. Blocked' t a -> a
ignoreBlocking (KanOperation -> Blocked (Arg Term)
kanOpCofib KanOperation
cmd), KanOperation -> Arg Term
kanOpBase KanOperation
cmd]

    forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. FamilyOrNot a -> a
famThing FamilyOrNot (Dom' Term Type, Abs Type)
ab)) (forall a. Abs a -> [Char]
absName forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. FamilyOrNot a -> a
famThing FamilyOrNot (Dom' Term Type, Abs Type)
ab) forall a b. (a -> b) -> a -> b
$ \NamesT ReduceM Term
u1 -> do
      case (KanOperation
cmd, FamilyOrNot (Dom' Term Type, Abs Type)
ab) of

        -- hcomp u u0 x = hcomp (λ i o → u i o x) (u0 x). Short and sweet :)
        (HCompOp Blocked (Arg Term)
_ Arg Term
u Arg Term
_, IsNot (Dom' Term Type
a , Abs Type
b)) -> do
          Type
bT <- (forall a. Subst a => Nat -> a -> a
raise Nat
1 Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp`) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT ReduceM Term
u1
          NamesT ReduceM Term
u <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (forall a. Subst a => Nat -> a -> a
raise Nat
1 (forall e. Arg e -> e
unArg Arg Term
u))
          forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp
            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Level' Term -> Term
Level forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {f :: * -> *} {a}.
(MonadReduce f, LensSort a) =>
a -> f (Level' Term)
toLevel Type
bT)
            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t a. Type'' t a -> a
unEl Type
bT)
            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT ReduceM Term
phi
            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\ NamesT ReduceM Term
i -> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT ReduceM Term
o -> forall (m :: * -> *).
Applicative m =>
Hiding -> m Term -> m Term -> m Term
gApply (forall a. LensHiding a => a -> Hiding
getHiding Dom' Term Type
a) (NamesT ReduceM Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT ReduceM Term
o) NamesT ReduceM Term
u1)
            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
Applicative m =>
Hiding -> m Term -> m Term -> m Term
gApply (forall a. LensHiding a => a -> Hiding
getHiding Dom' Term Type
a) NamesT ReduceM Term
u0 NamesT ReduceM Term
u1

        -- transp (λ i → (a : A i) → B i x) φ f u1 =
        --  transp (λ i → B i (transp (λ j → A (i ∨ ~ j)) (φ ∨ i) x)) φ
        --    (f (transp (λ j → A (~ j) φ x)))
        (TranspOp Blocked (Arg Term)
_ Arg Term
_, IsFam (Dom' Term Type
a , Abs Type
b)) -> do
          -- trA is a function of three arguments which builds the
          -- transport fillers in the opposite direction, hence its
          -- first argument is called "iOrNot" where it's relevant.
          let
            -- Γ , u1 : A[i1] , i : I
            v :: NamesT ReduceM Term -> NamesT ReduceM Term
v NamesT ReduceM Term
i = (NamesT ReduceM Term -> NamesT ReduceM Term)
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
trA (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT ReduceM Term
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg) (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT ReduceM Term
phi NamesT ReduceM Term
i) NamesT ReduceM Term
u1
            bB :: Term -> Type
bB Term
v = forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
v (forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 forall a b. (a -> b) -> a -> b
$ forall a. Nat -> Substitution' a
raiseS Nat
1) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
              (forall a. Subst a => Abs a -> a
absBody Abs Type
b {- Γ , i : I , x : A[i] -})

            -- Compute B @0 v, in the right scope
            tLam :: Abs Term -> Term
tLam = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo

          -- We know how to substitute v into B, but it's open in a
          -- variable, so we close over it here:
          Abs Type
bT <- forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT ReduceM b
x -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Type
bB forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamesT ReduceM Term -> NamesT ReduceM Term
v forall a b. (a -> b) -> a -> b
$ forall b. (Subst b, DeBruijn b) => NamesT ReduceM b
x

          forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTrans
            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Abs Term -> Term
tLam forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Level' Term -> Term
Level forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {f :: * -> *} {a}.
(MonadReduce f, LensSort a) =>
a -> f (Level' Term)
toLevel) Abs Type
bT)
            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Abs Term -> Term
tLam forall a b. (a -> b) -> a -> b
$ forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
bT)
            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
phi
            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
Applicative m =>
Hiding -> m Term -> m Term -> m Term
gApply (forall a. LensHiding a => a -> Hiding
getHiding Dom' Term Type
a) NamesT ReduceM Term
u0 (NamesT ReduceM Term -> NamesT ReduceM Term
v (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz))

        (KanOperation
_, FamilyOrNot (Dom' Term Type, Abs Type)
_) -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
"Invalid Kan operation in doPiKanOp"

-- | Compute Kan operations in a type of dependent paths.
doPathPKanOp
  :: KanOperation
  -> FamilyOrNot (Arg Term)
  -> FamilyOrNot (Arg Term, Arg Term, Arg Term)
  -> ReduceM (Reduced MaybeReducedArgs Term)
doPathPKanOp :: KanOperation
-> FamilyOrNot (Arg Term)
-> FamilyOrNot (Arg Term, Arg Term, Arg Term)
-> ReduceM (Reduced MaybeReducedArgs Term)
doPathPKanOp (HCompOp Blocked (Arg Term)
phi Arg Term
u Arg Term
u0) (IsNot Arg Term
l) (IsNot (Arg Term
bA,Arg Term
x,Arg Term
y)) = do
  let getTermLocal :: [Char] -> ReduceM Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm [Char]
"primHComp for path types"
  Term
tHComp <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinHComp

  forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
    [NamesT ReduceM Term
l, NamesT ReduceM Term
u, NamesT ReduceM Term
u0, NamesT ReduceM Term
phi, NamesT ReduceM Term
bA, NamesT ReduceM Term
x, NamesT ReduceM Term
y] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
l, Arg Term
u, Arg Term
u0, forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
phi, Arg Term
bA, Arg Term
x, Arg Term
y]

    -- hcomp in path spaces is simply hcomp in the underlying space, but
    -- fixing the endpoints at (j ∨ ~ j) in the new direction to those
    -- in the Path type.
    forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"j" forall a b. (a -> b) -> a -> b
$ \ NamesT ReduceM Term
j ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
j) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
phi forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
`imax` (forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT ReduceM Term
j forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
`imax` NamesT ReduceM Term
j))
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i'" (\NamesT ReduceM Term
i -> forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys NamesT ReduceM Term
l (NamesT ReduceM Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i)
          [ (NamesT ReduceM Term
phi,    forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\ NamesT ReduceM Term
o -> NamesT ReduceM Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT ReduceM Term
o forall (m :: * -> *).
Applicative m =>
m Term -> (m Term, m Term, m Term) -> m Term
<@@> (NamesT ReduceM Term
x, NamesT ReduceM Term
y, NamesT ReduceM Term
j)))
          , (NamesT ReduceM Term
j,      forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (forall a b. a -> b -> a
const NamesT ReduceM Term
y))
          , (forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT ReduceM Term
j, forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (forall a b. a -> b -> a
const NamesT ReduceM Term
x)) ])
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT ReduceM Term
u0 forall (m :: * -> *).
Applicative m =>
m Term -> (m Term, m Term, m Term) -> m Term
<@@> (NamesT ReduceM Term
x, NamesT ReduceM Term
y, NamesT ReduceM Term
j))

doPathPKanOp (TranspOp Blocked (Arg Term)
phi Arg Term
u0) (IsFam Arg Term
l) (IsFam (Arg Term
bA,Arg Term
x,Arg Term
y)) = do
  -- Γ    ⊢ l
  -- Γ, i ⊢ bA, x, y
  let getTermLocal :: [Char] -> ReduceM Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm [Char]
"transport for path types"
  Term
iz <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinIZero
  Term
io <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinIOne

  -- Transport in path types becomes /CCHM/ composition in the
  -- underlying line of spaces. The intuition is that not only do we
  -- have to fix the endpoints (using composition) but also actually
  -- transport. CCHM composition conveniently does that for us!

  forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
    -- In reality to avoid a round-trip between primComp we use mkComp
    -- here.
    NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
comp <- forall (m :: * -> *).
HasBuiltins m =>
[Char]
-> NamesT
     m
     (NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term)
mkComp forall a b. (a -> b) -> a -> b
$ [Char]
"transport for path types"
    [NamesT ReduceM Term
l, NamesT ReduceM Term
u0, NamesT ReduceM Term
phi] <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
l, Arg Term
u0, forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
phi]
    [NamesT ReduceM Term
bA, NamesT ReduceM Term
x, NamesT ReduceM Term
y] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ Arg Term
a -> forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Names -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a))) [Arg Term
bA, Arg Term
x, Arg Term
y]

    forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"j" forall a b. (a -> b) -> a -> b
$ \ NamesT ReduceM Term
j ->
      NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
comp NamesT ReduceM Term
l (forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT ReduceM Term
i -> NamesT ReduceM Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
j) (NamesT ReduceM Term
phi forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
`imax` (forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT ReduceM Term
j forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
`imax` NamesT ReduceM Term
j))
        (forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i'" forall a b. (a -> b) -> a -> b
$ \NamesT ReduceM Term
i -> forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys NamesT ReduceM Term
l (NamesT ReduceM Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
j)
          [ (NamesT ReduceM Term
phi, forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\NamesT ReduceM Term
o -> NamesT ReduceM Term
u0 forall (m :: * -> *).
Applicative m =>
m Term -> (m Term, m Term, m Term) -> m Term
<@@> (NamesT ReduceM Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz, NamesT ReduceM Term
y forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz, NamesT ReduceM Term
j)))
          -- Note that here we have lines of endpoints which we must
          -- apply to fix the endpoints:
          , (NamesT ReduceM Term
j,      forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"_" (forall a b. a -> b -> a
const (NamesT ReduceM Term
y forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i)))
          , (forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT ReduceM Term
j, forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"_" (forall a b. a -> b -> a
const (NamesT ReduceM Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i)))
          ])
        (NamesT ReduceM Term
u0 forall (m :: * -> *).
Applicative m =>
m Term -> (m Term, m Term, m Term) -> m Term
<@@> (NamesT ReduceM Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz, NamesT ReduceM Term
y forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz, NamesT ReduceM Term
j))
doPathPKanOp KanOperation
a0 FamilyOrNot (Arg Term)
_ FamilyOrNot (Arg Term, Arg Term, Arg Term)
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

redReturnNoSimpl :: a -> ReduceM (Reduced a' a)
redReturnNoSimpl :: forall a a'. a -> ReduceM (Reduced a' a)
redReturnNoSimpl = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
NoSimplification

primTransHComp :: Command -> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
primTransHComp :: Command
-> [Arg Term] -> Nat -> ReduceM (Reduced MaybeReducedArgs Term)
primTransHComp Command
cmd [Arg Term]
ts Nat
nelims = do
  (FamilyOrNot (Arg Term)
l,FamilyOrNot (Arg Term)
bA,Arg Term
phi,Maybe (Arg Term)
u,Arg Term
u0) <- forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case (Command
cmd,[Arg Term]
ts) of
    (Command
DoTransp, [Arg Term
l, Arg Term
bA, Arg Term
phi, Arg Term
u0]) -> (forall a. a -> FamilyOrNot a
IsFam Arg Term
l, forall a. a -> FamilyOrNot a
IsFam Arg Term
bA, Arg Term
phi, forall a. Maybe a
Nothing, Arg Term
u0)
    (Command
DoHComp, [Arg Term
l, Arg Term
bA, Arg Term
phi, Arg Term
u, Arg Term
u0]) -> (forall a. a -> FamilyOrNot a
IsNot Arg Term
l, forall a. a -> FamilyOrNot a
IsNot Arg Term
bA, Arg Term
phi, forall a. a -> Maybe a
Just Arg Term
u, Arg Term
u0)
    (Command, [Arg Term])
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
  Blocked (Arg Term)
sphi <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
  IntervalView
vphi <- forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sphi
  let clP :: [Char] -> m Term
clP [Char]
s = forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm [Char]
"primTransHComp" [Char]
s

  -- WORK
  case IntervalView
vphi of
    -- When φ = i1, we know what to do! These cases are counted as
    -- simplifications.
    IntervalView
IOne -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< case Command
cmd of
      Command
DoHComp -> forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
        -- If we're composing, then we definitely had a partial element
        -- to extend. But now it's just a total element, so we can
        -- just.. return it:
        NamesT ReduceM Term
u <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe (Arg Term)
u
        NamesT ReduceM Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall {m :: * -> *}. HasBuiltins m => [Char] -> m Term
clP [Char]
builtinIOne forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> forall {m :: * -> *}. HasBuiltins m => [Char] -> m Term
clP [Char]
builtinItIsOne
      Command
DoTransp ->
        -- Otherwise we're in the constant part of the line to transport
        -- over, so we must return the argument unchanged.
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
u0

    IntervalView
_ -> do
    let
      fallback' :: Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback' Blocked (Arg Term)
sc = do
        -- Possibly optimise the partial element to reduce the size of
        -- hcomps:
        MaybeReducedArgs
u' <- case Command
cmd of
          Command
DoHComp -> (forall a. a -> [a] -> [a]
:[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case IntervalView
vphi of
            -- If φ=i0 then tabulating equality for Partial φ A
            -- guarantees that u = is constantly isOneEmpty,
            -- regardless of how big the original term is, and
            -- isOneEmpty is *tiny*, so let's use that:
            IntervalView
IZero -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a t. a -> Blocked' t a
notBlocked forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. e -> Arg e
argN) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
                [NamesT ReduceM Term
l,NamesT ReduceM Term
c] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [forall a. FamilyOrNot a -> a
famThing FamilyOrNot (Arg Term)
l, forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sc]
                forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT ReduceM Term
i -> forall {m :: * -> *}. HasBuiltins m => [Char] -> m Term
clP [Char]
builtinIsOneEmpty forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\ NamesT ReduceM Term
_ -> NamesT ReduceM Term
c)

            -- Otherwise we have some interesting formula (though
            -- definitely not IOne!) and we have to keep the partial
            -- element as-is.
            IntervalView
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> MaybeReduced a
notReduced forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe (Arg Term)
u
          Command
DoTransp -> forall (m :: * -> *) a. Monad m => a -> m a
return []

        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ [forall a. a -> MaybeReduced a
notReduced (forall a. FamilyOrNot a -> a
famThing FamilyOrNot (Arg Term)
l), Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sc, Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi] forall a. [a] -> [a] -> [a]
++ MaybeReducedArgs
u' forall a. [a] -> [a] -> [a]
++ [forall a. a -> MaybeReduced a
notReduced Arg Term
u0]

    -- Reduce the type whose Kan operations we're composing over:
    Blocked (FamilyOrNot (Arg Term))
sbA <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' FamilyOrNot (Arg Term)
bA
    Maybe (Blocked' Term (FamilyOrNot Term))
t <- case forall e. Arg e -> e
unArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a. Blocked' t a -> a
ignoreBlocking Blocked (FamilyOrNot (Arg Term))
sbA of
      IsFam (Lam ArgInfo
_ Abs Term
t) -> forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> FamilyOrNot a
IsFam forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' (forall a. Subst a => Abs a -> a
absBody Abs Term
t)
      IsFam Term
_         -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
      IsNot Term
t         -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> FamilyOrNot a
IsNot forall a b. (a -> b) -> a -> b
$ (Term
t forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Blocked (FamilyOrNot (Arg Term))
sbA)

    case Maybe (Blocked' Term (FamilyOrNot Term))
t of
      -- If we don't have a grasp of the Kan operations then at least we
      -- can reuse the work we did for reducing the type later.
      Maybe (Blocked' Term (FamilyOrNot Term))
Nothing -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback' (forall a. FamilyOrNot a -> a
famThing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Blocked (FamilyOrNot (Arg Term))
sbA)
      Just Blocked' Term (FamilyOrNot Term)
st  -> do
        -- Similarly, if we're stuck for another reason, we can reuse
        -- the work for reducing the family.
        let
          fallback :: ReduceM (Reduced MaybeReducedArgs Term)
fallback = Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback' (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. FamilyOrNot a -> a
famThing forall a b. (a -> b) -> a -> b
$ Blocked' Term (FamilyOrNot Term)
st forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Blocked (FamilyOrNot (Arg Term))
sbA)
          t :: FamilyOrNot Term
t = forall t a. Blocked' t a -> a
ignoreBlocking Blocked' Term (FamilyOrNot Term)
st
          operation :: KanOperation
operation = case Command
cmd of
            Command
DoTransp -> TranspOp { kanOpCofib :: Blocked (Arg Term)
kanOpCofib = Blocked (Arg Term)
sphi, kanOpBase :: Arg Term
kanOpBase = Arg Term
u0 }
            Command
DoHComp -> HCompOp
              { kanOpCofib :: Blocked (Arg Term)
kanOpCofib = Blocked (Arg Term)
sphi, kanOpSides :: Arg Term
kanOpSides = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe (Arg Term)
u, kanOpBase :: Arg Term
kanOpBase = Arg Term
u0 }

        Maybe QName
mHComp <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getPrimitiveName' [Char]
builtinHComp
        Maybe QName
mGlue <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getPrimitiveName' [Char]
builtinGlue
        Maybe QName
mId   <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinId
        Type -> PathView
pathV <- forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView'

        -- By cases on the family, determine what Kan operation we defer
        -- to:
        case forall a. FamilyOrNot a -> a
famThing FamilyOrNot Term
t of
          -- Metavariables are stuck
          MetaV MetaId
m [Elim]
_ -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback' (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. FamilyOrNot a -> a
famThing forall a b. (a -> b) -> a -> b
$ forall t. MetaId -> Blocked' t ()
blocked_ MetaId
m forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Blocked (FamilyOrNot (Arg Term))
sbA)

          -- TODO: absName t instead of "i"
          Pi Dom' Term Type
a Abs Type
b
            -- For Π types, we prefer to keep the Kan operations around,
            -- so only actually reduce if we applied them to a nonzero
            -- positive of eliminations
            | Nat
nelims forall a. Ord a => a -> a -> Bool
> Nat
0 -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReduceM (Reduced MaybeReducedArgs Term)
fallback forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KanOperation
-> [Char]
-> FamilyOrNot (Dom' Term Type, Abs Type)
-> ReduceM (Maybe Term)
doPiKanOp KanOperation
operation [Char]
"i" ((Dom' Term Type
a, Abs Type
b) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ FamilyOrNot Term
t)
            | Bool
otherwise -> ReduceM (Reduced MaybeReducedArgs Term)
fallback

          -- For Type, we have two possibilities:
          Sort (Type Level' Term
l)
            -- transp (λ i → Type _) φ is always the identity function.
            | Command
DoTransp <- Command
cmd -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
u0
            -- hcomp {Type} is actually a normal form! This is the
            -- "HCompU" optimisation; We do not use Glue for hcomp in
            -- the universe.
            | Command
DoHComp <- Command
cmd -> ReduceM (Reduced MaybeReducedArgs Term)
fallback

          -- Glue types have their own implementation of Kan operations
          -- which are implemented in a different module:
          Def QName
q [Apply Arg Term
la, Apply Arg Term
lb, Apply Arg Term
bA, Apply Arg Term
phi', Apply Arg Term
bT, Apply Arg Term
e] | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mGlue -> do
            forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReduceM (Reduced MaybeReducedArgs Term)
fallback forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
PureTCM m =>
KanOperation
-> FamilyOrNot
     (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> m (Maybe Term)
doGlueKanOp
              KanOperation
operation ((Arg Term
la, Arg Term
lb, Arg Term
bA, Arg Term
phi', Arg Term
bT, Arg Term
e) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ FamilyOrNot Term
t) TermPosition
Head

          -- Formal homogeneous compositions in the universe: Our family
          -- is @hcomp {A = Type l}@, so we defer to the implementation
          -- of Kan operations for HCompU implemented above.
          Def QName
q [Apply Arg Term
_, Apply Arg Term
s, Apply Arg Term
phi', Apply Arg Term
bT, Apply Arg Term
bA]
            | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mHComp, Sort (Type Level' Term
la) <- forall e. Arg e -> e
unArg Arg Term
s  -> do
            forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReduceM (Reduced MaybeReducedArgs Term)
fallback forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
PureTCM m =>
KanOperation
-> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> m (Maybe Term)
doHCompUKanOp
              KanOperation
operation ((Level' Term -> Term
Level Level' Term
la forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Term
s, Arg Term
phi', Arg Term
bT, Arg Term
bA) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ FamilyOrNot Term
t) TermPosition
Head

          -- PathP types have the same optimisation as for Pi types:
          -- Only compute the Kan operation if there's >0 eliminations.
          Term
d | PathType Sort
_ QName
_ Arg Term
_ Arg Term
bA Arg Term
x Arg Term
y <- Type -> PathView
pathV (forall t a. Sort' t -> a -> Type'' t a
El HasCallStack => Sort
__DUMMY_SORT__ Term
d) -> do
            if Nat
nelims forall a. Ord a => a -> a -> Bool
> Nat
0 then KanOperation
-> FamilyOrNot (Arg Term)
-> FamilyOrNot (Arg Term, Arg Term, Arg Term)
-> ReduceM (Reduced MaybeReducedArgs Term)
doPathPKanOp KanOperation
operation FamilyOrNot (Arg Term)
l ((Arg Term
bA, Arg Term
x, Arg Term
y) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ FamilyOrNot Term
t) else ReduceM (Reduced MaybeReducedArgs Term)
fallback

          -- Identity types:
          Def QName
q [Apply Arg Term
_ , Apply Arg Term
bA , Apply Arg Term
x , Apply Arg Term
y] | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mId -> do
            forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReduceM (Reduced MaybeReducedArgs Term)
fallback forall (m :: * -> *) a. Monad m => a -> m a
return forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t.
KanOperation
-> FamilyOrNot (Arg Term)
-> FamilyOrNot (Arg Term, Arg Term, Arg Term)
-> ReduceM (Maybe (Reduced t Term))
doIdKanOp KanOperation
operation FamilyOrNot (Arg Term)
l ((Arg Term
bA, Arg Term
x, Arg Term
y) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ FamilyOrNot Term
t)

          Def QName
q [Elim]
es -> do
            Definition
info <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
            let   lam_i :: Term -> Term
lam_i = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
Abs [Char]
"i"

            -- Record and data types have their own implementations of
            -- the Kan operations, which get generated as part of their
            -- definition.
            case Definition -> Defn
theDef Definition
info of
              r :: Defn
r@Record{recComp :: Defn -> CompKit
recComp = CompKit
kit}
                | Nat
nelims forall a. Ord a => a -> a -> Bool
> Nat
0, Just [Arg Term]
as <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es, Command
DoTransp <- Command
cmd, Just QName
transpR <- CompKit -> Maybe QName
nameOfTransp CompKit
kit ->
                  -- Optimisation: If the record has no parameters then we can ditch the transport.
                  if Defn -> Nat
recPars Defn
r forall a. Eq a => a -> a -> Bool
== Nat
0
                     then forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
u0
                     else forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
transpR [] forall t. Apply t => t -> [Arg Term] -> t
`apply` (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
lam_i) [Arg Term]
as forall a. [a] -> [a] -> [a]
++ [forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sphi, Arg Term
u0])

                -- Records know how to hcomp themselves:
                | Nat
nelims forall a. Ord a => a -> a -> Bool
> Nat
0, Just [Arg Term]
as <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es, Command
DoHComp <- Command
cmd, Just QName
hCompR <- CompKit -> Maybe QName
nameOfHComp CompKit
kit ->
                  forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
hCompR [] forall t. Apply t => t -> [Arg Term] -> t
`apply` ([Arg Term]
as forall a. [a] -> [a] -> [a]
++ [forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sphi, forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe (Arg Term)
u,Arg Term
u0])

                -- If this is a record with no fields, then compData
                -- will know what to do with it:
                | Just [Arg Term]
as <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es, [] <- Defn -> [Dom QName]
recFields Defn
r -> forall {a}.
(Eq a, Num a, Pretty a) =>
Maybe QName
-> Bool
-> a
-> Command
-> FamilyOrNot (Arg Term)
-> FamilyOrNot [Arg Term]
-> Blocked (FamilyOrNot (Arg Term))
-> Blocked (Arg Term)
-> Maybe (Arg Term)
-> Arg Term
-> ReduceM (Reduced MaybeReducedArgs Term)
compData forall a. Maybe a
Nothing Bool
False (Defn -> Nat
recPars Defn
r) Command
cmd FamilyOrNot (Arg Term)
l ([Arg Term]
as forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ FamilyOrNot Term
t) Blocked (FamilyOrNot (Arg Term))
sbA Blocked (Arg Term)
sphi Maybe (Arg Term)
u Arg Term
u0

              -- For data types, if this data type is indexed and/or a
              -- higher inductive type, then hcomp is normal; But
              -- compData knows what to do for the general cases.
              Datatype{dataPars :: Defn -> Nat
dataPars = Nat
pars, dataIxs :: Defn -> Nat
dataIxs = Nat
ixs, dataPathCons :: Defn -> [QName]
dataPathCons = [QName]
pcons, dataTransp :: Defn -> Maybe QName
dataTransp = Maybe QName
mtrD}
                | forall (t :: * -> *). Foldable t => t Bool -> Bool
and [forall a. Null a => a -> Bool
null [QName]
pcons Bool -> Bool -> Bool
&& Nat
ixs forall a. Eq a => a -> a -> Bool
== Nat
0 | Command
DoHComp  <- [Command
cmd]], Just [Arg Term]
as <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es ->
                  forall {a}.
(Eq a, Num a, Pretty a) =>
Maybe QName
-> Bool
-> a
-> Command
-> FamilyOrNot (Arg Term)
-> FamilyOrNot [Arg Term]
-> Blocked (FamilyOrNot (Arg Term))
-> Blocked (Arg Term)
-> Maybe (Arg Term)
-> Arg Term
-> ReduceM (Reduced MaybeReducedArgs Term)
compData Maybe QName
mtrD ((Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null forall a b. (a -> b) -> a -> b
$ [QName]
pcons) Bool -> Bool -> Bool
|| Nat
ixs forall a. Ord a => a -> a -> Bool
> Nat
0) (Nat
parsforall a. Num a => a -> a -> a
+Nat
ixs) Command
cmd FamilyOrNot (Arg Term)
l ([Arg Term]
as forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ FamilyOrNot Term
t) Blocked (FamilyOrNot (Arg Term))
sbA Blocked (Arg Term)
sphi Maybe (Arg Term)
u Arg Term
u0

              -- Is this an axiom with constrant transport? Then. Well. Transport is constant.
              Axiom Bool
constTransp | Bool
constTransp, [] <- [Elim]
es, Command
DoTransp <- Command
cmd -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
u0

              Defn
_          -> ReduceM (Reduced MaybeReducedArgs Term)
fallback

          Term
_ -> ReduceM (Reduced MaybeReducedArgs Term)
fallback
  where
    allComponentsBack :: (IntervalView -> Term)
-> Term
-> Term
-> (Term -> a)
-> ReduceM ([a], [Maybe (Blocked' Term Term, IntMap Bool)])
allComponentsBack IntervalView -> Term
unview Term
phi Term
u Term -> a
p = do
            let
              boolToI :: Bool -> Term
boolToI Bool
b = if Bool
b then IntervalView -> Term
unview IntervalView
IOne else IntervalView -> Term
unview IntervalView
IZero
              lamlam :: Term -> Term
lamlam Term
t = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (forall a. [Char] -> a -> Abs a
Abs [Char]
"i" (ArgInfo -> Abs Term -> Term
Lam (forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant ArgInfo
defaultArgInfo) (forall a. [Char] -> a -> Abs a
Abs [Char]
"o" Term
t)))
            [(IntMap Bool, [Term])]
as <- forall (m :: * -> *).
HasBuiltins m =>
Term -> m [(IntMap Bool, [Term])]
decomposeInterval Term
phi
            ([a]
flags,[Maybe (Blocked' Term Term, IntMap Bool)]
t_alphas) <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. [(a, b)] -> ([a], [b])
unzip forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(IntMap Bool, [Term])]
as forall a b. (a -> b) -> a -> b
$ \ (IntMap Bool
bs,[Term]
ts) -> do
                 let u' :: Term
u' = forall a. EndoSubst a => [(Nat, a)] -> Substitution' a
listS [(Nat, Term)]
bs' forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
u
                     bs' :: [(Nat, Term)]
bs' = forall a. IntMap a -> [(Nat, a)]
IntMap.toAscList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map Bool -> Term
boolToI IntMap Bool
bs
                     -- Γ₁, i : I, Γ₂, j : I, Γ₃  ⊢ weaken : Γ₁, Γ₂, Γ₃   for bs' = [(j,_),(i,_)]
                     -- ordering of "j,i,.." matters.
                 let weaken :: Substitution' Term
weaken = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Nat
j Substitution' Term
s -> Substitution' Term
s forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall a. Nat -> Nat -> Substitution' a
raiseFromS Nat
j Nat
1) forall a. Substitution' a
idS (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Nat, Term)]
bs')
                 Blocked' Term Term
t <- Term -> ReduceM (Blocked' Term Term)
reduce2Lam Term
u'
                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Term -> a
p forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked' Term Term
t, forall a. [a] -> Maybe a
listToMaybe [ (Substitution' Term
weaken forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` (Term -> Term
lamlam forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Blocked' Term Term
t),IntMap Bool
bs) | forall a. Null a => a -> Bool
null [Term]
ts ])
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ([a]
flags,[Maybe (Blocked' Term Term, IntMap Bool)]
t_alphas)
    compData :: Maybe QName
-> Bool
-> a
-> Command
-> FamilyOrNot (Arg Term)
-> FamilyOrNot [Arg Term]
-> Blocked (FamilyOrNot (Arg Term))
-> Blocked (Arg Term)
-> Maybe (Arg Term)
-> Arg Term
-> ReduceM (Reduced MaybeReducedArgs Term)
compData Maybe QName
mtrD Bool
False a
_ cmd :: Command
cmd@Command
DoHComp (IsNot Arg Term
l) (IsNot [Arg Term]
ps) Blocked (FamilyOrNot (Arg Term))
fsc Blocked (Arg Term)
sphi (Just Arg Term
u) Arg Term
a0 = do
      let getTermLocal :: [Char] -> ReduceM Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm forall a b. (a -> b) -> a -> b
$ [Char]
"builtinHComp for data types"

      let sc :: Blocked (Arg Term)
sc = forall a. FamilyOrNot a -> a
famThing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Blocked (FamilyOrNot (Arg Term))
fsc
      Term
tEmpty <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinIsOneEmpty
      Term
tPOr   <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinPOr
      Term
iO   <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinIOne
      Term
iZ   <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinIZero
      Term
tMin <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinIMin
      Term
tNeg <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinINeg
      let iNeg :: Term -> Term
iNeg Term
t = Term
tNeg forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
t]
          iMin :: Term -> Term -> Term
iMin Term
t Term
u = Term
tMin forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
t, forall e. e -> Arg e
argN Term
u]
          iz :: NamesT ReduceM Term
iz = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iZ
      Term -> Term
constrForm <- do
        Maybe Term
mz <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getTerm' [Char]
builtinZero
        Maybe Term
ms <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getTerm' [Char]
builtinSuc
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ Term
t -> forall a. a -> Maybe a -> a
fromMaybe Term
t (forall (m :: * -> *).
Applicative m =>
m Term -> m Term -> Term -> m Term
constructorForm' Maybe Term
mz Maybe Term
ms Term
t)
      Blocked (Arg Term)
su  <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
u
      Blocked (Arg Term)
sa0 <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
a0
      Term -> IntervalView
view   <- forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
      IntervalView -> Term
unview <- forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
      let f :: Blocked' t (Arg c) -> c
f = forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Blocked' t a -> a
ignoreBlocking
          phi :: Term
phi = forall {t} {c}. Blocked' t (Arg c) -> c
f Blocked (Arg Term)
sphi
          a0 :: Term
a0 = forall {t} {c}. Blocked' t (Arg c) -> c
f Blocked (Arg Term)
sa0
          isLit :: Term -> Maybe Term
isLit t :: Term
t@(Lit Literal
lt) = forall a. a -> Maybe a
Just Term
t
          isLit Term
_ = forall a. Maybe a
Nothing
          isCon :: Term -> Maybe ConHead
isCon (Con ConHead
h ConInfo
_ [Elim]
_) = forall a. a -> Maybe a
Just ConHead
h
          isCon Term
_           = forall a. Maybe a
Nothing
          combine :: NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> [(NamesT ReduceM Term, NamesT ReduceM Term)]
-> NamesT ReduceM Term
combine NamesT ReduceM Term
l NamesT ReduceM Term
ty NamesT ReduceM Term
d [] = NamesT ReduceM Term
d
          combine NamesT ReduceM Term
l NamesT ReduceM Term
ty NamesT ReduceM Term
d [(NamesT ReduceM Term
psi,NamesT ReduceM Term
u)] = NamesT ReduceM Term
u
          combine NamesT ReduceM Term
l NamesT ReduceM Term
ty NamesT ReduceM Term
d ((NamesT ReduceM Term
psi,NamesT ReduceM Term
u):[(NamesT ReduceM Term, NamesT ReduceM Term)]
xs)
            = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tPOr forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
psi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) NamesT ReduceM Term
iz [(NamesT ReduceM Term, NamesT ReduceM Term)]
xs
                        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\ NamesT ReduceM Term
_ -> NamesT ReduceM Term
ty) -- the type
                        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> [(NamesT ReduceM Term, NamesT ReduceM Term)]
-> NamesT ReduceM Term
combine NamesT ReduceM Term
l NamesT ReduceM Term
ty NamesT ReduceM Term
d [(NamesT ReduceM Term, NamesT ReduceM Term)]
xs)
          noRed' :: Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
noRed' Blocked (Arg Term)
su = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction [forall a. a -> MaybeReduced a
notReduced Arg Term
l,Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sc, Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi, Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
su', Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sa0]
            where
              su' :: Blocked (Arg Term)
su' = case Term -> IntervalView
view Term
phi of
                     IntervalView
IZero -> forall a t. a -> Blocked' t a
notBlocked forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ forall a. Names -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ do
                                 [NamesT Fail Term
l,NamesT Fail Term
c] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
l,forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sc]
                                 forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
i -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tEmpty forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT Fail Term
l
                                                              forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\ NamesT Fail Term
_ -> NamesT Fail Term
c)
                     IntervalView
_     -> Blocked (Arg Term)
su
          sameConHeadBack :: Maybe Term
-> Maybe ConHead
-> Blocked (Arg Term)
-> (ConHead
    -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
sameConHeadBack Maybe Term
Nothing Maybe ConHead
Nothing Blocked (Arg Term)
su ConHead
-> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
k = Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
noRed' Blocked (Arg Term)
su
          sameConHeadBack Maybe Term
lt Maybe ConHead
h Blocked (Arg Term)
su ConHead
-> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
k = do
            let u :: Term
u = forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Blocked' t a -> a
ignoreBlocking forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
su
            ([(Bool, Bool)]
b, [Maybe (Blocked' Term Term, IntMap Bool)]
ts) <- forall {a}.
(IntervalView -> Term)
-> Term
-> Term
-> (Term -> a)
-> ReduceM ([a], [Maybe (Blocked' Term Term, IntMap Bool)])
allComponentsBack IntervalView -> Term
unview Term
phi Term
u forall a b. (a -> b) -> a -> b
$ \ Term
t ->
                        (Term -> Maybe Term
isLit Term
t forall a. Eq a => a -> a -> Bool
== Maybe Term
lt, Term -> Maybe ConHead
isCon (Term -> Term
constrForm Term
t) forall a. Eq a => a -> a -> Bool
== Maybe ConHead
h)
            let
              ([Bool]
lit,[Bool]
hd) = forall a b. [(a, b)] -> ([a], [b])
unzip [(Bool, Bool)]
b

            if forall a. Maybe a -> Bool
isJust Maybe Term
lt Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
lit then forall a a'. a -> ReduceM (Reduced a' a)
redReturn Term
a0 else do
            Blocked (Arg Term)
su <- forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe (Blocked' Term Term, IntMap Bool)]
ts) (forall (m :: * -> *) a. Monad m => a -> m a
return Blocked (Arg Term)
su) forall a b. (a -> b) -> a -> b
$ \ [(Blocked' Term Term, IntMap Bool)]
ts -> do
              let ([Blocked' Term Term]
us,[IntMap Bool]
bools) = forall a b. [(a, b)] -> ([a], [b])
unzip [(Blocked' Term Term, IntMap Bool)]
ts
              forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_ [Blocked' Term Term]
us forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. e -> Arg e
argN) forall a b. (a -> b) -> a -> b
$ do
              let
                phis :: [Term]
                phis :: [Term]
phis = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [IntMap Bool]
bools forall a b. (a -> b) -> a -> b
$ \ IntMap Bool
m ->
                            forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Term -> Term -> Term
iMin forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Nat
i,Bool
b) -> forall a. Bool -> (a -> a) -> a -> a
applyUnless Bool
b Term -> Term
iNeg forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
i)) Term
iO (forall a. IntMap a -> [(Nat, a)]
IntMap.toList IntMap Bool
m)
              forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
                NamesT ReduceM Term
u <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
u
                [NamesT ReduceM Term
l,NamesT ReduceM Term
c] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
l,forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sc]
                [NamesT ReduceM Term]
phis <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Term]
phis
                [NamesT ReduceM Term]
us   <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Blocked' t a -> a
ignoreBlocking) [Blocked' Term Term]
us
                forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT ReduceM Term
i -> do
                  NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> [(NamesT ReduceM Term, NamesT ReduceM Term)]
-> NamesT ReduceM Term
combine NamesT ReduceM Term
l NamesT ReduceM Term
c (NamesT ReduceM Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [NamesT ReduceM Term]
phis (forall a b. (a -> b) -> [a] -> [b]
map (\ NamesT ReduceM Term
t -> NamesT ReduceM Term
t forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i) [NamesT ReduceM Term]
us)

            if forall a. Maybe a -> Bool
isJust Maybe ConHead
h Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
hd then ConHead
-> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
k (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe ConHead
h) Blocked (Arg Term)
su
                      else Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
noRed' Blocked (Arg Term)
su

      Maybe Term
-> Maybe ConHead
-> Blocked (Arg Term)
-> (ConHead
    -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
sameConHeadBack (Term -> Maybe Term
isLit Term
a0) (Term -> Maybe ConHead
isCon Term
a0) Blocked (Arg Term)
su forall a b. (a -> b) -> a -> b
$ \ ConHead
h Blocked (Arg Term)
su -> do
            let u :: Term
u = forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Blocked' t a -> a
ignoreBlocking forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
su
            Constructor{ conComp :: Defn -> CompKit
conComp = CompKit
cm } <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
h)
            case CompKit -> Maybe QName
nameOfHComp CompKit
cm of
              Just QName
hcompD -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
hcompD [] forall t. Apply t => t -> [Arg Term] -> t
`apply`
                                          ([Arg Term]
ps forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall e. e -> Arg e
argN [Term
phi,Term
u,Term
a0])
              Maybe QName
Nothing        -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
noRed' Blocked (Arg Term)
su

    compData Maybe QName
mtrD        Bool
_     a
0     Command
DoTransp (IsFam Arg Term
l) (IsFam [Arg Term]
ps) Blocked (FamilyOrNot (Arg Term))
fsc Blocked (Arg Term)
sphi Maybe (Arg Term)
Nothing Arg Term
a0 = forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a0
    compData (Just QName
trD) Bool
isHIT a
_ cmd :: Command
cmd@Command
DoTransp (IsFam Arg Term
l) (IsFam [Arg Term]
ps) Blocked (FamilyOrNot (Arg Term))
fsc Blocked (Arg Term)
sphi Maybe (Arg Term)
Nothing Arg Term
a0 = do
      let sc :: Blocked (Arg Term)
sc = forall a. FamilyOrNot a -> a
famThing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Blocked (FamilyOrNot (Arg Term))
fsc
      let f :: Blocked' t (Arg c) -> c
f = forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Blocked' t a -> a
ignoreBlocking
          phi :: Term
          phi :: Term
phi = forall {t} {c}. Blocked' t (Arg c) -> c
f forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sphi
      let lam_i :: Term -> Term
lam_i = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
Abs [Char]
"i"
      forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
trD [] forall t. Apply t => t -> [Arg Term] -> t
`apply` (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
lam_i) [Arg Term]
ps forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall e. e -> Arg e
argN [Term
phi,forall e. Arg e -> e
unArg Arg Term
a0])

    compData Maybe QName
mtrD Bool
isHIT a
_ cmd :: Command
cmd@Command
DoTransp (IsFam Arg Term
l) (IsFam [Arg Term]
ps) Blocked (FamilyOrNot (Arg Term))
fsc Blocked (Arg Term)
sphi Maybe (Arg Term)
Nothing Arg Term
a0 = do
      let getTermLocal :: [Char] -> ReduceM Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm forall a b. (a -> b) -> a -> b
$ [Char]
builtinTrans forall a. [a] -> [a] -> [a]
++ [Char]
" for data types"
      let sc :: Blocked (Arg Term)
sc = forall a. FamilyOrNot a -> a
famThing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Blocked (FamilyOrNot (Arg Term))
fsc
      Maybe QName
mhcompName <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getName' [Char]
builtinHComp
      Term -> Term
constrForm <- do
        Maybe Term
mz <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getTerm' [Char]
builtinZero
        Maybe Term
ms <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getTerm' [Char]
builtinSuc
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ Term
t -> forall a. a -> Maybe a -> a
fromMaybe Term
t (forall (m :: * -> *).
Applicative m =>
m Term -> m Term -> Term -> m Term
constructorForm' Maybe Term
mz Maybe Term
ms Term
t)
      Blocked (Arg Term)
sa0 <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
a0
      let f :: Blocked' t (Arg c) -> c
f = forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Blocked' t a -> a
ignoreBlocking
          phi :: Term
phi = forall {t} {c}. Blocked' t (Arg c) -> c
f Blocked (Arg Term)
sphi
          a0 :: Term
a0 = forall {t} {c}. Blocked' t (Arg c) -> c
f Blocked (Arg Term)
sa0
          noRed :: ReduceM (Reduced MaybeReducedArgs Term)
noRed = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction [forall a. a -> MaybeReduced a
notReduced Arg Term
l,Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sc, Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi, Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sa0]
      let lam_i :: Term -> Term
lam_i = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
Abs [Char]
"i"
      case Term -> Term
constrForm Term
a0 of
        Con ConHead
h ConInfo
_ [Elim]
args -> do
          Constructor{ conComp :: Defn -> CompKit
conComp = CompKit
cm } <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
h)
          case CompKit -> Maybe QName
nameOfTransp CompKit
cm of
              Just QName
transpD -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
transpD [] forall t. Apply t => t -> [Arg Term] -> t
`apply`
                                          (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
lam_i) [Arg Term]
ps forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall e. e -> Arg e
argN [Term
phi,Term
a0])
              Maybe QName
Nothing        -> ReduceM (Reduced MaybeReducedArgs Term)
noRed
        Def QName
q [Elim]
es | Bool
isHIT, forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mhcompName, Just [Arg Term
_l0,Arg Term
_c0,Arg Term
psi,Arg Term
u,Arg Term
u0] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es -> do
           let bC :: Arg Term
bC = forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sc
           Term
hcomp <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinHComp
           Term
transp <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinTrans
           Term
io <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinIOne
           Term
iz <- [Char] -> ReduceM Term
getTermLocal [Char]
builtinIZero
           forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
             [NamesT ReduceM Term
l,NamesT ReduceM Term
bC,NamesT ReduceM Term
phi,NamesT ReduceM Term
psi,NamesT ReduceM Term
u,NamesT ReduceM Term
u0] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
l,Arg Term
bC,forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sphi,Arg Term
psi,Arg Term
u,Arg Term
u0]
             -- hcomp (sc 1) [psi |-> transp sc phi u] (transp sc phi u0)
             forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
hcomp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
bC forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT ReduceM Term
psi
                   forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"j" (\ NamesT ReduceM Term
j -> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT ReduceM Term
o ->
                        forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
transp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
bC forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT ReduceM Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
j forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT ReduceM Term
o))
                   forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
transp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
bC forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
u0)
        Term
_ -> ReduceM (Reduced MaybeReducedArgs Term)
noRed
    compData Maybe QName
mtrX Bool
isHITorIx a
nargs Command
cmd FamilyOrNot (Arg Term)
l FamilyOrNot [Arg Term]
t Blocked (FamilyOrNot (Arg Term))
sbA Blocked (Arg Term)
sphi Maybe (Arg Term)
u Arg Term
u0 = do
      () <- forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"compData" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat)
       [ TCMT IO Doc
"mtrX:       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Maybe QName
mtrX
       , TCMT IO Doc
"isHITorIx:  " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Bool
isHITorIx
       , TCMT IO Doc
"nargs:      " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
nargs
       , TCMT IO Doc
"cmd:        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Command
cmd)
       , TCMT IO Doc
"l:          " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall p a. IsString p => FamilyOrNot a -> p
familyOrNot FamilyOrNot (Arg Term)
l
       , TCMT IO Doc
"t:          " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall p a. IsString p => FamilyOrNot a -> p
familyOrNot FamilyOrNot [Arg Term]
t forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. FamilyOrNot a -> a
famThing FamilyOrNot [Arg Term]
t)
       , TCMT IO Doc
"sbA:          " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall p a. IsString p => FamilyOrNot a -> p
familyOrNot (forall t a. Blocked' t a -> a
ignoreBlocking forall a b. (a -> b) -> a -> b
$ Blocked (FamilyOrNot (Arg Term))
sbA)
       , TCMT IO Doc
"sphi:       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sphi)
       , TCMT IO Doc
"isJust u:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. Maybe a -> Bool
isJust Maybe (Arg Term)
u)
       , TCMT IO Doc
"u0:         " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Arg Term
u0
       ]
      forall a. HasCallStack => a
__IMPOSSIBLE__

--    compData _ _ _ _ _ _ _ _ _ _ = __IMPOSSIBLE__

-- | CCHM 'primComp' is implemented in terms of 'hcomp' and 'transport'.
-- The definition of it comes from 'mkComp'.
primComp :: TCM PrimitiveImpl
primComp :: TCM PrimitiveImpl
primComp = do
  Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
  Type
t    <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Functor m => m Term -> m Type
el (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"A" (forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i -> (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i))) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"φ" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
          forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType (\ NamesT (TCMT IO) Term
i -> forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
phi forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i) (NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i)) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
          (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) (NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne) (NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne))
  Term
one <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
  Term
io  <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Nat
-> ([Arg Term] -> Nat -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
PrimFun forall a. HasCallStack => a
__IMPOSSIBLE__ Nat
5 forall a b. (a -> b) -> a -> b
$ \ [Arg Term]
ts Nat
nelims -> do
    case [Arg Term]
ts of
      [Arg Term
l,Arg Term
c,Arg Term
phi,Arg Term
u,Arg Term
a0] -> do
        Blocked (Arg Term)
sphi <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
        IntervalView
vphi <- forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sphi
        case IntervalView
vphi of
          -- Though we short-circuit evaluation for the rule
          --    comp A i1 (λ _ .1=1 → u) u ==> u
          -- rather than going through the motions of hcomp and transp.
          IntervalView
IOne -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn (forall e. Arg e -> e
unArg Arg Term
u forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
io, forall e. e -> Arg e
argN Term
one])
          IntervalView
_    -> do
            forall a a'. a -> ReduceM (Reduced a' a)
redReturnNoSimpl forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
              NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
comp <- forall (m :: * -> *).
HasBuiltins m =>
[Char]
-> NamesT
     m
     (NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term)
mkComp [Char]
builtinComp
              [NamesT ReduceM Term
l,NamesT ReduceM Term
c,NamesT ReduceM Term
phi,NamesT ReduceM Term
u,NamesT ReduceM Term
a0] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
l,Arg Term
c,Arg Term
phi,Arg Term
u,Arg Term
a0]
              NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
comp NamesT ReduceM Term
l NamesT ReduceM Term
c NamesT ReduceM Term
phi NamesT ReduceM Term
u NamesT ReduceM Term
a0

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


-- TODO Andrea: keep reductions that happen under foralls?
primFaceForall' :: TCM PrimitiveImpl
primFaceForall' :: TCM PrimitiveImpl
primFaceForall' = do
  Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
  Type
t <- (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Nat
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Nat
1 forall a b. (a -> b) -> a -> b
$ \case
    [Arg Term
phi] -> do
      Blocked (Arg Term)
sphi <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
      case forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sphi of
        Lam ArgInfo
_ Abs Term
t -> do
          Abs Term
t <- forall t. Reduce t => t -> ReduceM t
reduce' Abs Term
t
          case Abs Term
t of
            NoAbs [Char]
_ Term
t -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn Term
t
            Abs [Char]
_ Term
t ->
              forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi]) forall a a'. a -> ReduceM (Reduced a' a)
redReturn
                forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall {m :: * -> *}. HasBuiltins m => Term -> m (Maybe Term)
toFaceMapsPrim Term
t
        Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall no yes. no -> Reduced no yes
NoReduction [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi])
    [Arg Term]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    toFaceMapsPrim :: Term -> m (Maybe Term)
toFaceMapsPrim Term
t = do
      Term -> IntervalView
view <- forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
      IntervalView -> Term
unview <- forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
      [(IntMap Bool, [Term])]
us' <- forall (m :: * -> *).
HasBuiltins m =>
Term -> m [(IntMap Bool, [Term])]
decomposeInterval Term
t
      Term
fr <- forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm [Char]
builtinFaceForall [Char]
builtinFaceForall
      let
        v :: IntervalView
v = Term -> IntervalView
view Term
t
        -- We decomposed the interval expression, without regard for
        -- inconsistent mappings, and now we keep only those which are
        -- stuck (the ts) and those which do not mention the 0th variable.
        us :: [[Either (Int, Bool) Term]]
        us :: [[Either (Nat, Bool) Term]]
us = [ forall a b. (a -> b) -> [a] -> [b]
map forall a b. a -> Either a b
Left (forall a. IntMap a -> [(Nat, a)]
IntMap.toList IntMap Bool
bsm) forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. b -> Either a b
Right [Term]
ts
             | (IntMap Bool
bsm, [Term]
ts) <- [(IntMap Bool, [Term])]
us', Nat
0 forall a. Nat -> IntMap a -> Bool
`IntMap.notMember` IntMap Bool
bsm
             ]

        -- Turn a face mapping back into an interval expression:
        fm :: (Nat, Bool) -> Term
fm (Nat
i, Bool
b) = if Bool
b then Nat -> Term
var (Nat
i forall a. Num a => a -> a -> a
- Nat
1) else IntervalView -> Term
unview (Arg Term -> IntervalView
INeg (forall e. e -> Arg e
argN (Nat -> Term
var forall a b. (a -> b) -> a -> b
$ Nat
i forall a. Num a => a -> a -> a
- Nat
1)))
        -- Apply ∀ to any indecomposable expressions we have encountered
        ffr :: Term -> Term
ffr Term
t = Term
fr forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> Abs a
Abs [Char]
"i" Term
t]

        -- Unfold one step of the foldr to avoid generation of the last
        -- ∧ i1. Marginal savings at best but it's cleaner.
        conjuncts :: [Either (Int, Bool) Term] -> Term
        conjuncts :: [Either (Nat, Bool) Term] -> Term
conjuncts [] = IntervalView -> Term
unview IntervalView
IOne
        conjuncts [Either (Nat, Bool) Term
x] = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Nat, Bool) -> Term
fm Term -> Term
ffr Either (Nat, Bool) Term
x
        conjuncts (Either (Nat, Bool) Term
x:[Either (Nat, Bool) Term]
xs) =
          forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Either (Nat, Bool) Term
x Term
r -> IntervalView -> Term
unview (Arg Term -> Arg Term -> IntervalView
IMin (forall e. e -> Arg e
argN (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Nat, Bool) -> Term
fm Term -> Term
ffr Either (Nat, Bool) Term
x)) (forall e. e -> Arg e
argN Term
r)))
            (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Nat, Bool) -> Term
fm Term -> Term
ffr Either (Nat, Bool) Term
x)
            [Either (Nat, Bool) Term]
xs

        disjuncts :: Term
disjuncts = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
          (\[Either (Nat, Bool) Term]
conj Term
rest -> IntervalView -> Term
unview (Arg Term -> Arg Term -> IntervalView
IMax (forall e. e -> Arg e
argN ([Either (Nat, Bool) Term] -> Term
conjuncts [Either (Nat, Bool) Term]
conj)) (forall e. e -> Arg e
argN Term
rest)))
          (IntervalView -> Term
unview IntervalView
IZero)
          [[Either (Nat, Bool) Term]]
us
      --   traceSLn "cube.forall" 20 (unlines [show v, show us', show us, show r]) $
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case [(IntMap Bool, [Term])]
us' of
        [(IntMap Bool
m, [Term
_])] | forall a. Null a => a -> Bool
null IntMap Bool
m -> forall a. Maybe a
Nothing
        [(IntMap Bool, [Term])]
_ -> forall a. a -> Maybe a
Just Term
disjuncts

-- | Tries to @primTransp@ a whole telescope of arguments, following the rule for Σ types.
--   If a type in the telescope does not support transp, @transpTel@ throws it as an exception.
transpTel :: Abs Telescope -- Γ ⊢ i.Δ
          -> Term          -- Γ ⊢ φ : F  -- i.Δ const on φ
          -> Args          -- Γ ⊢ δ : Δ[0]
          -> ExceptT (Closure (Abs Type)) TCM Args      -- Γ ⊢ Δ[1]
transpTel :: Abs Telescope
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term]
transpTel = forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
transpTel' Bool
False


transpTel' :: (PureTCM m, MonadError TCErr m) =>
          Bool -> Abs Telescope -- Γ ⊢ i.Δ
          -> Term          -- Γ ⊢ φ : F  -- i.Δ const on φ
          -> Args          -- Γ ⊢ δ : Δ[0]
          -> ExceptT (Closure (Abs Type)) m Args      -- Γ ⊢ Δ[1]
transpTel' :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
transpTel' Bool
flag Abs Telescope
delta Term
phi [Arg Term]
args = forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> [(Term, Abs [Term])]
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
transpSysTel' Bool
flag Abs Telescope
delta [] Term
phi [Arg Term]
args

type LM m a = NamesT (ExceptT (Closure (Abs Type)) m) a
-- transporting with an extra system/partial element
-- or composing when some of the system is known to be constant.
transpSysTel' :: forall m. (PureTCM m, MonadError TCErr m) =>
          Bool
          -> Abs Telescope -- Γ ⊢ i.Δ
          -> [(Term,Abs [Term])] -- [(ψ,i.δ)] with  Γ,ψ ⊢ i.δ : [i : I]. Δ[i]  -- the proof of [ψ] is not in scope.
          -> Term          -- Γ ⊢ φ : F  -- i.Δ const on φ and all i.δ const on φ ∧ ψ
          -> Args          -- Γ ⊢ δ : Δ[0]
          -> ExceptT (Closure (Abs Type)) m Args      -- Γ ⊢ Δ[1]
transpSysTel' :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> [(Term, Abs [Term])]
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
transpSysTel' Bool
flag Abs Telescope
delta [(Term, Abs [Term])]
us Term
phi [Arg Term]
args = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"cubical.prim.transpTel" Nat
20 forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"transpSysTel'"
          , (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"delta  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Char]
"i" :: String, HasCallStack => Dom' Term Type
__DUMMY_DOM__) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. Abs a -> a
unAbs Abs Telescope
delta)
--          , (text "us =" <+>) $ nest 2 $ prettyList $ map prettyTCM us
          , (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"phi    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
phi
          , (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"args   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
args
          ]
  let getTermLocal :: [Char] -> ExceptT (Closure (Abs Type)) m Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm [Char]
"transpSys"
  Term
tTransp <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans
  Term
tComp <- [Char] -> ExceptT (Closure (Abs Type)) m Term
getTermLocal [Char]
builtinComp
  Term
tPOr <- [Char] -> ExceptT (Closure (Abs Type)) m Term
getTermLocal [Char]
builtinPOr
  Term
iz <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
  Term
imin <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin
  Term
imax <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax
  Term
ineg <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
  let
    noTranspError :: Abs a -> t m b
noTranspError Abs a
t = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"cubical.prim.transpTel" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"error type =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$
        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Char]
"i" :: String, HasCallStack => Dom' Term Type
__DUMMY_DOM__) forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> a
unAbs Abs a
t
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Abs a
t
    bapp :: forall m a. (Applicative m, Subst a) => m (Abs a) -> m (SubstArg a) -> m a
    bapp :: forall (m :: * -> *) a.
(Applicative m, Subst a) =>
m (Abs a) -> m (SubstArg a) -> m a
bapp m (Abs a)
t m (SubstArg a)
u = forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Abs a)
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (SubstArg a)
u
    doGTransp :: NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
-> [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
     NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
doGTransp NamesT (ExceptT (Closure (Abs Type)) m) Term
l NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
us NamesT (ExceptT (Closure (Abs Type)) m) Term
phi NamesT (ExceptT (Closure (Abs Type)) m) Term
a | forall a. Null a => a -> Bool
null [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
us = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTransp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (ExceptT (Closure (Abs Type)) m) Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
a
                           | Bool
otherwise = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (ExceptT (Closure (Abs Type)) m) Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (ExceptT (Closure (Abs Type)) m) Term
face forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
uphi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
a
      where
        -- [phi -> a; us]
        face :: NamesT (ExceptT (Closure (Abs Type)) m) Term
face = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ NamesT (ExceptT (Closure (Abs Type)) m) Term
x NamesT (ExceptT (Closure (Abs Type)) m) Term
y -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
imax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
y) (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz) (NamesT (ExceptT (Closure (Abs Type)) m) Term
phi forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
us)
        uphi :: NamesT (ExceptT (Closure (Abs Type)) m) Term
uphi = forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT (ExceptT (Closure (Abs Type)) m) Term
i -> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (ExceptT (Closure (Abs Type)) m) Term
o -> do
          let sys' :: [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) Term)]
sys' = (NamesT (ExceptT (Closure (Abs Type)) m) Term
phi , NamesT (ExceptT (Closure (Abs Type)) m) Term
a) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (forall (m :: * -> *) a.
(Applicative m, Subst a) =>
m (Abs a) -> m (SubstArg a) -> m a
`bapp` NamesT (ExceptT (Closure (Abs Type)) m) Term
i)) [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
us
              sys :: [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) Term)]
sys = forall a b. (a -> b) -> [a] -> [b]
map (forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const) [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) Term)]
sys'
          NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
     NamesT (ExceptT (Closure (Abs Type)) m) Term)]
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
combine (NamesT (ExceptT (Closure (Abs Type)) m) Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
i) (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(Applicative m, Subst a) =>
m (Abs a) -> m (SubstArg a) -> m a
bapp NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t NamesT (ExceptT (Closure (Abs Type)) m) Term
i) forall a. HasCallStack => a
__IMPOSSIBLE__ [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) Term)]
sys forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (ExceptT (Closure (Abs Type)) m) Term
o
    combine :: NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
     NamesT (ExceptT (Closure (Abs Type)) m) Term)]
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
combine NamesT (ExceptT (Closure (Abs Type)) m) Term
l NamesT (ExceptT (Closure (Abs Type)) m) Term
ty NamesT (ExceptT (Closure (Abs Type)) m) Term
d [] = NamesT (ExceptT (Closure (Abs Type)) m) Term
d
    combine NamesT (ExceptT (Closure (Abs Type)) m) Term
l NamesT (ExceptT (Closure (Abs Type)) m) Term
ty NamesT (ExceptT (Closure (Abs Type)) m) Term
d [(NamesT (ExceptT (Closure (Abs Type)) m) Term
psi,NamesT (ExceptT (Closure (Abs Type)) m) Term
u)] = NamesT (ExceptT (Closure (Abs Type)) m) Term
u
    combine NamesT (ExceptT (Closure (Abs Type)) m) Term
l NamesT (ExceptT (Closure (Abs Type)) m) Term
ty NamesT (ExceptT (Closure (Abs Type)) m) Term
d ((NamesT (ExceptT (Closure (Abs Type)) m) Term
psi,NamesT (ExceptT (Closure (Abs Type)) m) Term
u):[(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) Term)]
xs)
            = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tPOr forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (ExceptT (Closure (Abs Type)) m) Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
psi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ NamesT (ExceptT (Closure (Abs Type)) m) Term
x NamesT (ExceptT (Closure (Abs Type)) m) Term
y -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
imax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
y) (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) Term)]
xs))
                        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (ExceptT (Closure (Abs Type)) m) Term
_ -> NamesT (ExceptT (Closure (Abs Type)) m) Term
ty) -- the type
                        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
     NamesT (ExceptT (Closure (Abs Type)) m) Term)]
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
combine NamesT (ExceptT (Closure (Abs Type)) m) Term
l NamesT (ExceptT (Closure (Abs Type)) m) Term
ty NamesT (ExceptT (Closure (Abs Type)) m) Term
d [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) Term)]
xs)

    gTransp :: Maybe (LM m Term) -> LM m (Abs Type) -> [(LM m Term,LM m (Abs Term))] -> LM m Term -> LM m Term -> LM m Term
    gTransp :: Maybe (NamesT (ExceptT (Closure (Abs Type)) m) Term)
-> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
-> [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
     NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
gTransp (Just NamesT (ExceptT (Closure (Abs Type)) m) Term
l) NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
u NamesT (ExceptT (Closure (Abs Type)) m) Term
phi NamesT (ExceptT (Closure (Abs Type)) m) Term
a
     | Bool
flag = do
      Abs Type
t' <- NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t
      [Abs Term]
us' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a b. (a, b) -> b
snd [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
u
      case ( Nat
0 forall a. Free a => Nat -> a -> Bool
`freeIn` (forall a. Subst a => Nat -> a -> a
raise Nat
1 Abs Type
t' forall a. Subst a => Abs a -> SubstArg a -> a
`lazyAbsApp` Nat -> Term
var Nat
0)
           , Nat
0 forall a. Free a => Nat -> a -> Bool
`freeIn` forall a b. (a -> b) -> [a] -> [b]
map (\ Abs Term
u -> forall a. Subst a => Nat -> a -> a
raise Nat
1 Abs Term
u forall a. Subst a => Abs a -> SubstArg a -> a
`lazyAbsApp` Nat -> Term
var Nat
0) [Abs Term]
us'
           ) of
        (Bool
False,Bool
False) -> NamesT (ExceptT (Closure (Abs Type)) m) Term
a
        (Bool
False,Bool
True)  -> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
-> [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
     NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
doGTransp NamesT (ExceptT (Closure (Abs Type)) m) Term
l NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
u NamesT (ExceptT (Closure (Abs Type)) m) Term
phi NamesT (ExceptT (Closure (Abs Type)) m) Term
a -- TODO? optimize to "hcomp (l <@> io) (bapp t io) ((phi,NoAbs a):u) a" ?
        (Bool
True,Bool
_) -> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
-> [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
     NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
doGTransp NamesT (ExceptT (Closure (Abs Type)) m) Term
l NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
u NamesT (ExceptT (Closure (Abs Type)) m) Term
phi NamesT (ExceptT (Closure (Abs Type)) m) Term
a
     | Bool
otherwise = NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
-> [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
     NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
doGTransp NamesT (ExceptT (Closure (Abs Type)) m) Term
l NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
u NamesT (ExceptT (Closure (Abs Type)) m) Term
phi NamesT (ExceptT (Closure (Abs Type)) m) Term
a

    gTransp Maybe (NamesT (ExceptT (Closure (Abs Type)) m) Term)
Nothing NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
sys NamesT (ExceptT (Closure (Abs Type)) m) Term
phi NamesT (ExceptT (Closure (Abs Type)) m) Term
a = do
      let ([NamesT (ExceptT (Closure (Abs Type)) m) Term]
psis,[NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term)]
us) = forall a b. [(a, b)] -> ([a], [b])
unzip [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
sys
      -- Γ ⊢ i.Ξ
      NamesT (ExceptT (Closure (Abs Type)) m) (Abs Telescope)
xi <- (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i -> do
          TelV Telescope
xi Type
_ <- (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall a b. (a -> b) -> a -> b
$ NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t forall (m :: * -> *) a.
(Applicative m, Subst a) =>
m (Abs a) -> m (SubstArg a) -> m a
`bapp` forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i
          forall (m :: * -> *) a. Monad m => a -> m a
return Telescope
xi
      [Arg [Char]]
argnames <- do
        Telescope -> [Arg [Char]]
teleArgNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Abs a -> a
unAbs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Telescope)
xi
      forall (m :: * -> *).
(Functor m, MonadFail m) =>
[Arg [Char]]
-> (NamesT m [Arg Term] -> NamesT m Term) -> NamesT m Term
glamN [Arg [Char]]
argnames forall a b. (a -> b) -> a -> b
$ \ NamesT (ExceptT (Closure (Abs Type)) m) [Arg Term]
xi_args -> do
        Abs Type
b' <- forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i -> do
          Type
ti <- NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t forall (m :: * -> *) a.
(Applicative m, Subst a) =>
m (Abs a) -> m (SubstArg a) -> m a
`bapp` forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i
          Abs Telescope
xin <- forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i -> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Telescope)
xi forall (m :: * -> *) a.
(Applicative m, Subst a) =>
m (Abs a) -> m (SubstArg a) -> m a
`bapp` (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
ineg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i)
          [Arg Term]
xi_args <- NamesT (ExceptT (Closure (Abs Type)) m) [Arg Term]
xi_args
          Term
ni <- forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
ineg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i
          Term
phi <- NamesT (ExceptT (Closure (Abs Type)) m) Term
phi
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
ti forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) m [Arg Term]
trFillTel' Bool
flag Abs Telescope
xin Term
phi [Arg Term]
xi_args Term
ni
        [Abs Term]
usxi <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term)]
us forall a b. (a -> b) -> a -> b
$ \ NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term)
u -> forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i -> do
          Term
ui <- NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term)
u forall (m :: * -> *) a.
(Applicative m, Subst a) =>
m (Abs a) -> m (SubstArg a) -> m a
`bapp` forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i
          Abs Telescope
xin <- forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i -> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Telescope)
xi forall (m :: * -> *) a.
(Applicative m, Subst a) =>
m (Abs a) -> m (SubstArg a) -> m a
`bapp` (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
ineg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i)
          [Arg Term]
xi_args <- NamesT (ExceptT (Closure (Abs Type)) m) [Arg Term]
xi_args
          Term
ni <- forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
ineg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i
          Term
phi <- NamesT (ExceptT (Closure (Abs Type)) m) Term
phi
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall t. Apply t => t -> [Arg Term] -> t
apply Term
ui forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) m [Arg Term]
trFillTel' Bool
flag Abs Telescope
xin Term
phi [Arg Term]
xi_args Term
ni
        Term
axi <- do
          Term
a <- NamesT (ExceptT (Closure (Abs Type)) m) Term
a
          Abs Telescope
xif <- forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i -> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Telescope)
xi forall (m :: * -> *) a.
(Applicative m, Subst a) =>
m (Abs a) -> m (SubstArg a) -> m a
`bapp` (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
ineg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i)
          Term
phi <- NamesT (ExceptT (Closure (Abs Type)) m) Term
phi
          [Arg Term]
xi_args <- NamesT (ExceptT (Closure (Abs Type)) m) [Arg Term]
xi_args
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall t. Apply t => t -> [Arg Term] -> t
apply Term
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
transpTel' Bool
flag Abs Telescope
xif Term
phi [Arg Term]
xi_args
        Sort
s <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort (forall a. Subst a => Abs a -> a
absBody Abs Type
b')
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"cubical.transp" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. Subst a => Nat -> a -> a
raise Nat
1 Abs Type
b' forall a. Subst a => Abs a -> SubstArg a -> a
`lazyAbsApp` Nat -> Term
var Nat
0)
        let noTranspSort :: NamesT (ExceptT (Closure (Abs Type)) m) Term
noTranspSort = if Nat
0 forall a. Free a => Nat -> a -> Bool
`freeIn` (forall a. Subst a => Nat -> a -> a
raise Nat
1 Abs Type
b' forall a. Subst a => Abs a -> SubstArg a -> a
`lazyAbsApp` Nat -> Term
var Nat
0) Bool -> Bool -> Bool
|| Nat
0 forall a. Free a => Nat -> a -> Bool
`freeIn` (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Subst a => Abs a -> SubstArg a -> a
`lazyAbsApp` Nat -> Term
var Nat
0) (forall a. Subst a => Nat -> a -> a
raise Nat
1 [Abs Term]
usxi))
              then forall {t :: (* -> *) -> * -> *} {m :: * -> *} {a} {b}.
(MonadDebug (t m), PrettyTCM a, MonadTrans t,
 MonadError (Closure (Abs a)) m, MonadTCEnv (t m),
 ReadTCState (t m)) =>
Abs a -> t m b
noTranspError Abs Type
b'
              else forall (m :: * -> *) a. Monad m => a -> m a
return Term
axi

        case Sort
s of
          Type Level' Term
l -> do
            NamesT (ExceptT (Closure (Abs Type)) m) Term
l <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ Term -> Term
lam_i (Level' Term -> Term
Level Level' Term
l)
            NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
b' <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Abs Type
b'
            NamesT (ExceptT (Closure (Abs Type)) m) Term
axi <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
axi
            [NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term)]
usxi <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Abs Term]
usxi
            Maybe (NamesT (ExceptT (Closure (Abs Type)) m) Term)
-> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
-> [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
     NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
gTransp (forall a. a -> Maybe a
Just NamesT (ExceptT (Closure (Abs Type)) m) Term
l) NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
b' (forall a b. [a] -> [b] -> [(a, b)]
zip [NamesT (ExceptT (Closure (Abs Type)) m) Term]
psis [NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term)]
usxi) NamesT (ExceptT (Closure (Abs Type)) m) Term
phi NamesT (ExceptT (Closure (Abs Type)) m) Term
axi
          Inf IsFibrant
_ Integer
n  -> NamesT (ExceptT (Closure (Abs Type)) m) Term
noTranspSort
          SSet Level' Term
_  -> NamesT (ExceptT (Closure (Abs Type)) m) Term
noTranspSort
          Sort
SizeUniv -> NamesT (ExceptT (Closure (Abs Type)) m) Term
noTranspSort
          Sort
LockUniv -> NamesT (ExceptT (Closure (Abs Type)) m) Term
noTranspSort
          Sort
IntervalUniv -> NamesT (ExceptT (Closure (Abs Type)) m) Term
noTranspSort
          Prop{}  -> NamesT (ExceptT (Closure (Abs Type)) m) Term
noTranspSort
          Sort
_ -> forall {t :: (* -> *) -> * -> *} {m :: * -> *} {a} {b}.
(MonadDebug (t m), PrettyTCM a, MonadTrans t,
 MonadError (Closure (Abs a)) m, MonadTCEnv (t m),
 ReadTCState (t m)) =>
Abs a -> t m b
noTranspError Abs Type
b'
    lam_i :: Term -> Term
lam_i = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
Abs [Char]
"i"
    go :: Telescope -> [[(Term,Term)]] -> Term -> Args -> ExceptT (Closure (Abs Type)) m Args
    go :: Telescope
-> [[(Term, Term)]]
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
go Telescope
EmptyTel            [] Term
_  []       = forall (m :: * -> *) a. Monad m => a -> m a
return []
    go (ExtendTel Dom' Term Type
t Abs Telescope
delta) ([(Term, Term)]
u:[[(Term, Term)]]
us) Term
phi (Arg Term
a:[Arg Term]
args) = do
      -- Γ,i ⊢ t
      -- Γ,i ⊢ (x : t). delta
      -- Γ ⊢ a : t[0]
      Sort
s <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort Dom' Term Type
t
      -- Γ ⊢ b : t[1]    Γ, i ⊢ bf : t[i]
      (Term
b,Term
bf) <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
        Maybe (NamesT (ExceptT (Closure (Abs Type)) m) Term)
l <- case Sort
s of
               SSet Level' Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
               Sort
IntervalUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
               Sort
SizeUniv     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
               Sort
LockUniv     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
               Inf IsFibrant
_ Integer
n -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
               Type Level' Term
l -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> Term
lam_i (Level' Term -> Term
Level Level' Term
l))
               Sort
_ -> forall {t :: (* -> *) -> * -> *} {m :: * -> *} {a} {b}.
(MonadDebug (t m), PrettyTCM a, MonadTrans t,
 MonadError (Closure (Abs a)) m, MonadTCEnv (t m),
 ReadTCState (t m)) =>
Abs a -> t m b
noTranspError (forall a. [Char] -> a -> Abs a
Abs [Char]
"i" (forall t e. Dom' t e -> e
unDom Dom' Term Type
t))
        NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> Abs a
Abs [Char]
"i" (forall t e. Dom' t e -> e
unDom Dom' Term Type
t)
        [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
u <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Term, Term)]
u forall a b. (a -> b) -> a -> b
$ \ (Term
psi,Term
upsi) -> do
              (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
psi forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (forall a. [Char] -> a -> Abs a
Abs [Char]
"i" Term
upsi)
        [NamesT (ExceptT (Closure (Abs Type)) m) Term
phi,NamesT (ExceptT (Closure (Abs Type)) m) Term
a] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Term
phi, forall e. Arg e -> e
unArg Arg Term
a]
        Term
b <- Maybe (NamesT (ExceptT (Closure (Abs Type)) m) Term)
-> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
-> [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
     NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
gTransp Maybe (NamesT (ExceptT (Closure (Abs Type)) m) Term)
l NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
u NamesT (ExceptT (Closure (Abs Type)) m) Term
phi NamesT (ExceptT (Closure (Abs Type)) m) Term
a
        Abs Term
bf <- forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i -> do
                            Maybe (NamesT (ExceptT (Closure (Abs Type)) m) Term)
-> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
-> [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
     NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
-> NamesT (ExceptT (Closure (Abs Type)) m) Term
gTransp ((forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (NamesT (ExceptT (Closure (Abs Type)) m) Term)
l) forall a b. (a -> b) -> a -> b
$ \ NamesT (ExceptT (Closure (Abs Type)) m) Term
l -> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"j" forall a b. (a -> b) -> a -> b
$ \ NamesT (ExceptT (Closure (Abs Type)) m) Term
j -> NamesT (ExceptT (Closure (Abs Type)) m) Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
imin forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
j))
                                    (forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"j" forall a b. (a -> b) -> a -> b
$ \ forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
j -> NamesT (ExceptT (Closure (Abs Type)) m) (Abs Type)
t forall (m :: * -> *) a.
(Applicative m, Subst a) =>
m (Abs a) -> m (SubstArg a) -> m a
`bapp` (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
imin forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
j))
                                    [(NamesT (ExceptT (Closure (Abs Type)) m) Term,
  NamesT (ExceptT (Closure (Abs Type)) m) (Abs Term))]
u
                                    (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
imax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
ineg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b.
(Subst b, DeBruijn b) =>
NamesT (ExceptT (Closure (Abs Type)) m) b
i) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (ExceptT (Closure (Abs Type)) m) Term
phi)
                                    NamesT (ExceptT (Closure (Abs Type)) m) Term
a
        forall (m :: * -> *) a. Monad m => a -> m a
return (Term
b, forall a. Subst a => Abs a -> a
absBody Abs Term
bf)
      (:) (Term
b forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Term
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope
-> [[(Term, Term)]]
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
go (forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp Abs Telescope
delta Term
bf) [[(Term, Term)]]
us Term
phi [Arg Term]
args
    go Telescope
EmptyTel            [[(Term, Term)]]
_ Term
_ [Arg Term]
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
    go (ExtendTel Dom' Term Type
t Abs Telescope
delta) [[(Term, Term)]]
_ Term
_ [Arg Term]
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
  let ([Term]
psis,[Abs [Term]]
uss) = forall a b. [(a, b)] -> ([a], [b])
unzip [(Term, Abs [Term])]
us
      us' :: [[(Term, Term)]]
us' | forall a. Null a => a -> Bool
null [(Term, Abs [Term])]
us = forall a. Nat -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg Term]
args) []
          | Bool
otherwise = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
psis) forall a b. (a -> b) -> a -> b
$ forall a. [[a]] -> [[a]]
List.transpose (forall a b. (a -> b) -> [a] -> [b]
map forall a. Subst a => Abs a -> a
absBody [Abs [Term]]
uss)
  Telescope
-> [[(Term, Term)]]
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
go (forall a. Subst a => Abs a -> a
absBody Abs Telescope
delta) [[(Term, Term)]]
us' Term
phi [Arg Term]
args

-- | Like @transpTel@ but performing a transpFill.
trFillTel :: Abs Telescope -- Γ ⊢ i.Δ
          -> Term
          -> Args          -- Γ ⊢ δ : Δ[0]
          -> Term          -- Γ ⊢ r : I
          -> ExceptT (Closure (Abs Type)) TCM Args      -- Γ ⊢ Δ[r]
trFillTel :: Abs Telescope
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) (TCMT IO) [Arg Term]
trFillTel = forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) m [Arg Term]
trFillTel' Bool
False

trFillTel' :: (PureTCM m, MonadError TCErr m) =>
          Bool
          -> Abs Telescope -- Γ ⊢ i.Δ
          -> Term
          -> Args          -- Γ ⊢ δ : Δ[0]
          -> Term          -- Γ ⊢ r : I
          -> ExceptT (Closure (Abs Type)) m Args      -- Γ ⊢ Δ[r]
trFillTel' :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> Term
-> ExceptT (Closure (Abs Type)) m [Arg Term]
trFillTel' Bool
flag Abs Telescope
delta Term
phi [Arg Term]
args Term
r = do
  Term
imin <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin
  Term
imax <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax
  Term
ineg <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
  forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
transpTel' Bool
flag (forall a. [Char] -> a -> Abs a
Abs [Char]
"j" forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
1 Abs Telescope
delta forall a. Subst a => Abs a -> SubstArg a -> a
`lazyAbsApp` (Term
imin forall t. Apply t => t -> [Arg Term] -> t
`apply` (forall a b. (a -> b) -> [a] -> [b]
map forall e. e -> Arg e
argN [Nat -> Term
var Nat
0, forall a. Subst a => Nat -> a -> a
raise Nat
1 Term
r])))
            (Term
imax forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ Term
ineg forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
r], forall e. e -> Arg e
argN Term
phi])
            [Arg Term]
args



-- hcompTel' :: Bool -> Telescope -> [(Term,Abs [Term])] -> [Term] -> ExceptT (Closure (Abs Type)) TCM [Term]
-- hcompTel' b delta sides base = undefined

-- hFillTel' :: Bool -> Telescope -- Γ ⊢ Δ
--           -> [(Term,Abs [Term])]  -- [(φ,i.δ)] with  Γ,φ ⊢ i.δ : I → Δ
--           -> [Term]            -- Γ ⊢ δ0 : Δ, matching the [(φ,i.δ)]
--           -> Term -- Γ ⊢ r : I
--           -> ExceptT (Closure (Abs Type)) TCM [Term]
-- hFillTel' b delta sides base = undefined

pathTelescope
  :: forall m. (PureTCM m, MonadError TCErr m) =>
  Telescope -- Δ
  -> [Arg Term] -- lhs : Δ
  -> [Arg Term] -- rhs : Δ
  -> m Telescope
pathTelescope :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
pathTelescope Telescope
tel [Arg Term]
lhs [Arg Term]
rhs = do
  Either (Closure Type) Telescope
x <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (forall (m :: * -> *).
(PureTCM m, MonadError (Closure Type) m) =>
Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
pathTelescope' Telescope
tel [Arg Term]
lhs [Arg Term]
rhs)
  case Either (Closure Type) Telescope
x of
    Left Closure Type
t -> do
      forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t forall a b. (a -> b) -> a -> b
$ \ Type
t ->
                 forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                    (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"The sort of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"should be of the form \"Set l\"")
    Right Telescope
tel -> forall (m :: * -> *) a. Monad m => a -> m a
return Telescope
tel

pathTelescope'
  :: forall m. (PureTCM m, MonadError (Closure Type) m) =>
  Telescope -- Δ
  -> [Arg Term] -- lhs : Δ
  -> [Arg Term] -- rhs : Δ
  -> m Telescope
pathTelescope' :: forall (m :: * -> *).
(PureTCM m, MonadError (Closure Type) m) =>
Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
pathTelescope' Telescope
tel [Arg Term]
lhs [Arg Term]
rhs = do
  Term
pathp <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getTerm' [Char]
builtinPathP
  Term -> Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
go Term
pathp (forall a. Subst a => Nat -> a -> a
raise Nat
1 Telescope
tel) [Arg Term]
lhs [Arg Term]
rhs
 where
  -- Γ,i ⊢ Δ, Γ ⊢ lhs : Δ[0], Γ ⊢ rhs : Δ[1]
  go :: Term -> Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
  go :: Term -> Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
go Term
pathp (ExtendTel Dom' Term Type
a Abs Telescope
tel) (Arg Term
u : [Arg Term]
lhs) (Arg Term
v : [Arg Term]
rhs) = do
    let t :: Type
t = forall t e. Dom' t e -> e
unDom Dom' Term Type
a
    Level' Term
l <- forall a. Subst a => Nat -> SubstArg a -> a -> a
subst Nat
0 HasCallStack => Term
__DUMMY_TERM__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (Level' Term)
getLevel Type
t
    let a' :: Type
a' = forall t a. Sort' t -> a -> Type'' t a
El (forall t. Level' t -> Sort' t
Type Level' Term
l) (forall t. Apply t => t -> [Arg Term] -> t
apply Term
pathp forall a b. (a -> b) -> a -> b
$ [forall e. e -> Arg e
argH forall a b. (a -> b) -> a -> b
$ Level' Term -> Term
Level Level' Term
l] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall e. e -> Arg e
argN [ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (forall a. [Char] -> a -> Abs a
Abs [Char]
"i" forall a b. (a -> b) -> a -> b
$ forall t a. Type'' t a -> a
unEl Type
t), forall e. Arg e -> e
unArg Arg Term
u, forall e. Arg e -> e
unArg Arg Term
v])
        -- Γ,eq : u ≡ v, i : I ⊢ m = eq i : t[i]
        -- m  = runNames [] $ do
        --        [u,v] <- mapM (open . unArg) [u,v]
        --        bind "eq" $ \ eq -> bind "i" $ \ i ->
    (forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type
a' forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom' Term Type
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
      let nm :: [Char]
nm = (forall a. Abs a -> [Char]
absName Abs Telescope
tel)
      NamesT m (Abs (Abs Telescope))
tel <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> Abs a
Abs [Char]
"i" Abs Telescope
tel
      [NamesT m Term
u,NamesT m Term
v] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
u,Arg Term
v]
      [NamesT m [Arg Term]
lhs,NamesT m [Arg Term]
rhs] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [[Arg Term]
lhs,[Arg Term]
rhs]
      forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
nm forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT m b
eq -> do
        [Arg Term]
lhs <- NamesT m [Arg Term]
lhs
        [Arg Term]
rhs <- NamesT m [Arg Term]
rhs
        Abs Telescope
tel' <- forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT m b
i ->
                  forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m (Abs (Abs Telescope))
tel forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall b. (Subst b, DeBruijn b) => NamesT m b
i) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall b. (Subst b, DeBruijn b) => NamesT m b
eq forall (m :: * -> *).
Applicative m =>
m Term -> (m Term, m Term, m Term) -> m Term
<@@> (NamesT m Term
u, NamesT m Term
v, forall b. (Subst b, DeBruijn b) => NamesT m b
i))
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Term -> Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
go Term
pathp (forall a. Subst a => Abs a -> a
absBody Abs Telescope
tel') [Arg Term]
lhs [Arg Term]
rhs
  go Term
_ Telescope
EmptyTel [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Tele a
EmptyTel
  go Term
_ Telescope
_ [Arg Term]
_ [Arg Term]
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
  getLevel :: Type -> m Level
  getLevel :: Type -> m (Level' Term)
getLevel Type
t = do
    Sort
s <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort Type
t
    case Sort
s of
      Type Level' Term
l -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Level' Term
l
      Sort
s      -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Type
t

data TranspError = CannotTransp {TranspError -> Closure (Abs Type)
errorType :: (Closure (Abs Type)) }

instance Exception TranspError
instance Show TranspError where
  show :: TranspError -> [Char]
show TranspError
_ = [Char]
"TranspError"

tryTranspError :: TCM a -> TCM (Either (Closure (Abs Type)) a)
tryTranspError :: forall a. TCM a -> TCM (Either (Closure (Abs Type)) a)
tryTranspError (TCM IORef TCState -> TCEnv -> IO a
m) = forall (m :: * -> *) a. (IORef TCState -> TCEnv -> m a) -> TCMT m a
TCM forall a b. (a -> b) -> a -> b
$ \ IORef TCState
s TCEnv
env -> do
  forall a c b. (a -> c) -> Either a b -> Either c b
mapLeft TranspError -> Closure (Abs Type)
errorType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall e a. Exception e => IO a -> IO (Either e a)
try (IORef TCState -> TCEnv -> IO a
m IORef TCState
s TCEnv
env))

transpPathPTel' ::
             NamesT TCM (Abs (Abs Telescope)) -- ^ j.i.Δ                 const on φ
             -> [NamesT TCM Term]          -- ^ x : (i : I) → Δ[0,i]  const on φ
             -> [NamesT TCM Term]          -- ^ y : (i : I) → Δ[1,i]  const on φ
             -> NamesT TCM Term            -- ^ φ
             -> [NamesT TCM Term]          -- ^ p : PathP (λ j → Δ[j,0]) (x 0) (y 0)
             -> NamesT TCM [Arg Term] -- PathP (λ j → Δ[j,0]) (x 1) (y 1) [ φ ↦ q ]
transpPathPTel' :: NamesT (TCMT IO) (Abs (Abs Telescope))
-> [NamesT (TCMT IO) Term]
-> [NamesT (TCMT IO) Term]
-> NamesT (TCMT IO) Term
-> [NamesT (TCMT IO) Term]
-> NamesT (TCMT IO) [Arg Term]
transpPathPTel' NamesT (TCMT IO) (Abs (Abs Telescope))
theTel [NamesT (TCMT IO) Term]
x [NamesT (TCMT IO) Term]
y NamesT (TCMT IO) Term
phi [NamesT (TCMT IO) Term]
p = do
 let neg :: NamesT m Term -> NamesT m Term
neg NamesT m Term
j = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
j
 -- is the open overkill?
 NamesT (TCMT IO) [Arg Term]
qs <- (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Abs [Char]
n (Arg ArgInfo
i Term
t)) -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> Abs a
Abs [Char]
n Term
t)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA)
                  forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"j" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
j -> do
   Abs Telescope
theTel <- forall a. Subst a => Abs a -> SubstArg a -> a
absApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs (Abs Telescope))
theTel forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
j
   [Term]
faces <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term
neg forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
j, forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
j]
   [Abs [Term]]
us <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [[NamesT (TCMT IO) Term]
x,[NamesT (TCMT IO) Term]
y] forall a b. (a -> b) -> a -> b
$ \ [NamesT (TCMT IO) Term]
z -> do
           forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NamesT (TCMT IO) Term]
z (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i)
   let sys :: [(Term, Abs [Term])]
sys = forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
faces [Abs [Term]]
us
   -- [(neg j, bind "i" $ \ i -> flip map x (<@> i))
   -- ,(j , bind "i" $ \ i -> flip map y (<@> i))]
   Term
phi <- NamesT (TCMT IO) Term
phi
   [Term]
p0 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
j) [NamesT (TCMT IO) Term]
p
   let toArgs :: [Term] -> [Arg Term]
toArgs = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg [Char]
a Term
t -> Term
t forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg [Char]
a) (Telescope -> [Arg [Char]]
teleArgNames (forall a. Abs a -> a
unAbs forall a b. (a -> b) -> a -> b
$ Abs Telescope
theTel))
   Either (Closure (Abs Type)) [Arg Term]
eq <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> [(Term, Abs [Term])]
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
transpSysTel' Bool
False Abs Telescope
theTel [(Term, Abs [Term])]
sys Term
phi ([Term] -> [Arg Term]
toArgs [Term]
p0)
   forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a e. Exception e => e -> a
throw forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure (Abs Type) -> TranspError
CannotTransp) forall (f :: * -> *) a. Applicative f => a -> f a
pure Either (Closure (Abs Type)) [Arg Term]
eq
 NamesT (TCMT IO) [Arg Term]
qs

transpPathTel' ::
             NamesT TCM (Abs Telescope) -- ^ i.Δ                 const on φ
             -> [NamesT TCM Term]          -- ^ x : (i : I) → Δ[i]  const on φ
             -> [NamesT TCM Term]          -- ^ y : (i : I) → Δ[i]  const on φ
             -> NamesT TCM Term            -- ^ φ
             -> [NamesT TCM Term]          -- ^ p : Path (Δ[0]) (x 0) (y 0)
             -> NamesT TCM [Arg Term] -- Path (Δ[1]) (x 1) (y 1) [ φ ↦ q ]
transpPathTel' :: NamesT (TCMT IO) (Abs Telescope)
-> [NamesT (TCMT IO) Term]
-> [NamesT (TCMT IO) Term]
-> NamesT (TCMT IO) Term
-> [NamesT (TCMT IO) Term]
-> NamesT (TCMT IO) [Arg Term]
transpPathTel' NamesT (TCMT IO) (Abs Telescope)
theTel [NamesT (TCMT IO) Term]
x [NamesT (TCMT IO) Term]
y NamesT (TCMT IO) Term
phi [NamesT (TCMT IO) Term]
p = do
 let neg :: NamesT m Term -> NamesT m Term
neg NamesT m Term
j = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
j
 -- is the open overkill?
 NamesT (TCMT IO) [Arg Term]
qs <- (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Abs [Char]
n (Arg ArgInfo
i Term
t)) -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> Abs a
Abs [Char]
n Term
t)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA)
                  forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"j" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
j -> do
   Abs Telescope
theTel <- NamesT (TCMT IO) (Abs Telescope)
theTel
   [Term]
faces <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$ [forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term
neg forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
j, forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
j]
   [Abs [Term]]
us <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [[NamesT (TCMT IO) Term]
x,[NamesT (TCMT IO) Term]
y] forall a b. (a -> b) -> a -> b
$ \ [NamesT (TCMT IO) Term]
z -> do
           forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NamesT (TCMT IO) Term]
z (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i)
   let sys :: [(Term, Abs [Term])]
sys = forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
faces [Abs [Term]]
us
   -- [(neg j, bind "i" $ \ i -> flip map x (<@> i))
   -- ,(j , bind "i" $ \ i -> flip map y (<@> i))]
   Term
phi <- NamesT (TCMT IO) Term
phi
   [Term]
p0 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
j) [NamesT (TCMT IO) Term]
p
   let toArgs :: [Term] -> [Arg Term]
toArgs = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg [Char]
a Term
t -> Term
t forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg [Char]
a) (Telescope -> [Arg [Char]]
teleArgNames (forall a. Abs a -> a
unAbs Abs Telescope
theTel))
   Either (Closure (Abs Type)) [Arg Term]
eq <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Bool
-> Abs Telescope
-> [(Term, Abs [Term])]
-> Term
-> [Arg Term]
-> ExceptT (Closure (Abs Type)) m [Arg Term]
transpSysTel' Bool
False Abs Telescope
theTel [(Term, Abs [Term])]
sys Term
phi ([Term] -> [Arg Term]
toArgs [Term]
p0)
   forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a e. Exception e => e -> a
throw forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure (Abs Type) -> TranspError
CannotTransp) forall (f :: * -> *) a. Applicative f => a -> f a
pure Either (Closure (Abs Type)) [Arg Term]
eq
 NamesT (TCMT IO) [Arg Term]
qs

trFillPathTel' ::
               NamesT TCM (Abs Telescope) -- ^ i.Δ                 const on φ
             -> [NamesT TCM Term]          -- ^ x : (i : I) → Δ[i]  const on φ
             -> [NamesT TCM Term]          -- ^ y : (i : I) → Δ[i]  const on φ
             -> NamesT TCM Term            -- ^ φ
             -> [NamesT TCM Term]          -- ^ p : Path (Δ[0]) (x 0) (y 0)
             -> NamesT TCM Term            -- ^ r
             -> NamesT TCM [Arg Term] -- Path (Δ[r]) (x r) (y r) [ φ ↦ q; (r = 0) ↦ q ]
trFillPathTel' :: NamesT (TCMT IO) (Abs Telescope)
-> [NamesT (TCMT IO) Term]
-> [NamesT (TCMT IO) Term]
-> NamesT (TCMT IO) Term
-> [NamesT (TCMT IO) Term]
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) [Arg Term]
trFillPathTel' NamesT (TCMT IO) (Abs Telescope)
tel [NamesT (TCMT IO) Term]
x [NamesT (TCMT IO) Term]
y NamesT (TCMT IO) Term
phi [NamesT (TCMT IO) Term]
p NamesT (TCMT IO) Term
r = do
  let max :: NamesT m Term -> NamesT m Term -> NamesT m Term
max NamesT m Term
i NamesT m Term
j = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
j
  let min :: NamesT m Term -> NamesT m Term -> NamesT m Term
min NamesT m Term
i NamesT m Term
j = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
j
  let neg :: NamesT m Term -> NamesT m Term
neg NamesT m Term
i = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i
  [NamesT (TCMT IO) Term]
x' <- (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Monad m =>
NamesT m (Abs [Term]) -> NamesT m [Term]
lamTel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NamesT (TCMT IO) Term]
x (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term -> NamesT m Term
min NamesT (TCMT IO) Term
r forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i))
  [NamesT (TCMT IO) Term]
y' <- (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Monad m =>
NamesT m (Abs [Term]) -> NamesT m [Term]
lamTel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NamesT (TCMT IO) Term]
y (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term -> NamesT m Term
min NamesT (TCMT IO) Term
r forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i))
  NamesT (TCMT IO) (Abs Telescope)
-> [NamesT (TCMT IO) Term]
-> [NamesT (TCMT IO) Term]
-> NamesT (TCMT IO) Term
-> [NamesT (TCMT IO) Term]
-> NamesT (TCMT IO) [Arg Term]
transpPathTel' (forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i -> forall a. Subst a => Abs a -> SubstArg a -> a
absApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs Telescope)
tel forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term -> NamesT m Term
min NamesT (TCMT IO) Term
r forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i)
                 [NamesT (TCMT IO) Term]
x'
                 [NamesT (TCMT IO) Term]
y'
                 (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term -> NamesT m Term
max NamesT (TCMT IO) Term
phi (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term
neg NamesT (TCMT IO) Term
r))
                 [NamesT (TCMT IO) Term]
p

trFillPathPTel' ::
               NamesT TCM (Abs (Abs Telescope)) -- ^ j.i.Δ                 const on φ
             -> [NamesT TCM Term]          -- ^ x : (i : I) → Δ[0,i]  const on φ
             -> [NamesT TCM Term]          -- ^ y : (i : I) → Δ[1,i]  const on φ
             -> NamesT TCM Term            -- ^ φ
             -> [NamesT TCM Term]          -- ^ p : Path (\ j -> Δ[j,0]) (x 0) (y 0)
             -> NamesT TCM Term            -- ^ r
             -> NamesT TCM [Arg Term] -- Path (\ j → Δ[j,r]) (x r) (y r) [ φ ↦ q; (r = 0) ↦ q ]
trFillPathPTel' :: NamesT (TCMT IO) (Abs (Abs Telescope))
-> [NamesT (TCMT IO) Term]
-> [NamesT (TCMT IO) Term]
-> NamesT (TCMT IO) Term
-> [NamesT (TCMT IO) Term]
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) [Arg Term]
trFillPathPTel' NamesT (TCMT IO) (Abs (Abs Telescope))
tel [NamesT (TCMT IO) Term]
x [NamesT (TCMT IO) Term]
y NamesT (TCMT IO) Term
phi [NamesT (TCMT IO) Term]
p NamesT (TCMT IO) Term
r = do
  let max :: NamesT m Term -> NamesT m Term -> NamesT m Term
max NamesT m Term
i NamesT m Term
j = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
j
  let min :: NamesT m Term -> NamesT m Term -> NamesT m Term
min NamesT m Term
i NamesT m Term
j = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
j
  let neg :: NamesT m Term -> NamesT m Term
neg NamesT m Term
i = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i
  [NamesT (TCMT IO) Term]
x' <- (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Monad m =>
NamesT m (Abs [Term]) -> NamesT m [Term]
lamTel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NamesT (TCMT IO) Term]
x (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term -> NamesT m Term
min NamesT (TCMT IO) Term
r forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i))
  [NamesT (TCMT IO) Term]
y' <- (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Monad m =>
NamesT m (Abs [Term]) -> NamesT m [Term]
lamTel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NamesT (TCMT IO) Term]
y (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term -> NamesT m Term
min NamesT (TCMT IO) Term
r forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i))
  NamesT (TCMT IO) (Abs (Abs Telescope))
-> [NamesT (TCMT IO) Term]
-> [NamesT (TCMT IO) Term]
-> NamesT (TCMT IO) Term
-> [NamesT (TCMT IO) Term]
-> NamesT (TCMT IO) [Arg Term]
transpPathPTel' (forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"j" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
j -> forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i -> forall a. Subst a => Abs a -> SubstArg a -> a
absApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. Subst a => Abs a -> SubstArg a -> a
absApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs (Abs Telescope))
tel forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
j) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term -> NamesT m Term
min NamesT (TCMT IO) Term
r forall b. (Subst b, DeBruijn b) => NamesT (TCMT IO) b
i)
                 [NamesT (TCMT IO) Term]
x'
                 [NamesT (TCMT IO) Term]
y'
                 (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term -> NamesT m Term
max NamesT (TCMT IO) Term
phi (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term
neg NamesT (TCMT IO) Term
r))
                 [NamesT (TCMT IO) Term]
p



-- given Γ ⊢ I type, and Γ ⊢ Δ telescope, build Δ^I such that
-- Γ ⊢ (x : A, y : B x, ...)^I = (x : I → A, y : (i : I) → B (x i), ...)
expTelescope :: Type -> Telescope -> Telescope
expTelescope :: Type -> Telescope -> Telescope
expTelescope Type
int Telescope
tel = Names -> [Dom' Term Type] -> Telescope
unflattenTel Names
names [Dom' Term Type]
ys
  where
    stel :: Nat
stel = forall a. Sized a => a -> Nat
size Telescope
tel
    xs :: [Dom' Term Type]
xs = forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel
    names :: Names
names = Telescope -> Names
teleNames Telescope
tel
    t :: Telescope
t = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (forall a. a -> Dom a
defaultDom forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
stel Type
int) (forall a. [Char] -> a -> Abs a
Abs [Char]
"i" forall a. Tele a
EmptyTel)
    s :: Substitution' Term
s = Nat -> Substitution' Term
expS Nat
stel
    ys :: [Dom' Term Type]
ys = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. Abstract t => Telescope -> t -> t
abstract Telescope
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
s) [Dom' Term Type]
xs


-- | Γ, Δ^I, i : I |- expS |Δ| : Γ, Δ
expS :: Nat -> Substitution
expS :: Nat -> Substitution' Term
expS Nat
stel = forall a.
DeBruijn a =>
Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS forall a. HasCallStack => a
__IMPOSSIBLE__
  [ forall a. a -> Maybe a
Just (Nat -> Term
var Nat
n forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
0]) | Nat
n <- [Nat
1..Nat
stel] ]
  (forall a. Nat -> Substitution' a
raiseS (Nat
stel forall a. Num a => a -> a -> a
+ Nat
1))


-- * Special cases of Type
-----------------------------------------------------------

-- | A @Type@ with sort @Type l@
--   Such a type supports both hcomp and transp.
data LType = LEl Level Term deriving (LType -> LType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LType -> LType -> Bool
$c/= :: LType -> LType -> Bool
== :: LType -> LType -> Bool
$c== :: LType -> LType -> Bool
Eq,Nat -> LType -> ShowS
[LType] -> ShowS
LType -> [Char]
forall a.
(Nat -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [LType] -> ShowS
$cshowList :: [LType] -> ShowS
show :: LType -> [Char]
$cshow :: LType -> [Char]
showsPrec :: Nat -> LType -> ShowS
$cshowsPrec :: Nat -> LType -> ShowS
Show)

fromLType :: LType -> Type
fromLType :: LType -> Type
fromLType (LEl Level' Term
l Term
t) = forall t a. Sort' t -> a -> Type'' t a
El (forall t. Level' t -> Sort' t
Type Level' Term
l) Term
t

lTypeLevel :: LType -> Level
lTypeLevel :: LType -> Level' Term
lTypeLevel (LEl Level' Term
l Term
t) = Level' Term
l

toLType :: MonadReduce m => Type -> m (Maybe LType)
toLType :: forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
toLType Type
ty = do
  Sort
sort <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort Type
ty
  case Sort
sort of
    Type Level' Term
l -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Level' Term -> Term -> LType
LEl Level' Term
l (forall t a. Type'' t a -> a
unEl Type
ty)
    Sort
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing

instance Subst LType where
  type SubstArg LType = Term
  applySubst :: Substitution' (SubstArg LType) -> LType -> LType
applySubst Substitution' (SubstArg LType)
rho (LEl Level' Term
l Term
t) = Level' Term -> Term -> LType
LEl (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg LType)
rho Level' Term
l) (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg LType)
rho Term
t)

-- | A @Type@ that either has sort @Type l@ or is a closed definition.
--   Such a type supports some version of transp.
--   In particular we want to allow the Interval as a @ClosedType@.
data CType = ClosedType Sort QName | LType LType deriving (CType -> CType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CType -> CType -> Bool
$c/= :: CType -> CType -> Bool
== :: CType -> CType -> Bool
$c== :: CType -> CType -> Bool
Eq,Nat -> CType -> ShowS
[CType] -> ShowS
CType -> [Char]
forall a.
(Nat -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [CType] -> ShowS
$cshowList :: [CType] -> ShowS
show :: CType -> [Char]
$cshow :: CType -> [Char]
showsPrec :: Nat -> CType -> ShowS
$cshowsPrec :: Nat -> CType -> ShowS
Show)

instance P.Pretty CType where
  pretty :: CType -> Doc
pretty = forall a. Pretty a => a -> Doc
P.pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
fromCType

fromCType :: CType -> Type
fromCType :: CType -> Type
fromCType (ClosedType Sort
s QName
q) = forall t a. Sort' t -> a -> Type'' t a
El Sort
s (QName -> [Elim] -> Term
Def QName
q [])
fromCType (LType LType
t) = LType -> Type
fromLType LType
t

toCType :: MonadReduce m => Type -> m (Maybe CType)
toCType :: forall (m :: * -> *). MonadReduce m => Type -> m (Maybe CType)
toCType Type
ty = do
  Sort
sort <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort Type
ty
  case Sort
sort of
    Type Level' Term
l -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ LType -> CType
LType (Level' Term -> Term -> LType
LEl Level' Term
l (forall t a. Type'' t a -> a
unEl Type
ty))
    SSet{} -> do
      Term
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t a. Type'' t a -> a
unEl Type
ty)
      case Term
t of
        Def QName
q [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Sort -> QName -> CType
ClosedType Sort
sort QName
q
        Term
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing
    Sort
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing

instance Subst CType where
  type SubstArg CType = Term
  applySubst :: Substitution' (SubstArg CType) -> CType -> CType
applySubst Substitution' (SubstArg CType)
rho (ClosedType Sort
s QName
q) = Sort -> QName -> CType
ClosedType (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg CType)
rho Sort
s) QName
q
  applySubst Substitution' (SubstArg CType)
rho (LType LType
t) = LType -> CType
LType forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg CType)
rho LType
t

hcomp
  :: (HasBuiltins m, MonadError TCErr m, MonadReduce m, MonadPretty m)
  => NamesT m Type
  -> [(NamesT m Term, NamesT m Term)]
  -> NamesT m Term
  -> NamesT m Term
hcomp :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadReduce m,
 MonadPretty m) =>
NamesT m Type
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
-> NamesT m Term
hcomp NamesT m Type
ty [(NamesT m Term, NamesT m Term)]
sys NamesT m Term
u0 = do
  Term
iz <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
  Term
tHComp <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHComp
  let max :: NamesT m Term -> NamesT m Term -> NamesT m Term
max NamesT m Term
i NamesT m Term
j = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
j
  Type
ty <- NamesT m Type
ty
  (Level' Term
l, Term
ty) <- forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
toLType Type
ty forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just (LEl Level' Term
l Term
ty) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Level' Term
l, Term
ty)
    Maybe LType
Nothing -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ do -- TODO: support Setω properly
      forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Cubical Agda: cannot generate hcomp clauses at type", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ty ]
  NamesT m Term
l <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ Level' Term -> Term
Level Level' Term
l
  NamesT m Term
ty <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ Term
ty
  Term
face <- (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term -> NamesT m Term
max (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ [(NamesT m Term, NamesT m Term)]
sys)
  Term
sys <- forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i'" forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
i -> forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys NamesT m Term
l NamesT m Term
ty [(NamesT m Term
phi, NamesT m Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) | (NamesT m Term
phi,NamesT m Term
u) <- [(NamesT m Term, NamesT m Term)]
sys]
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
ty forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
face forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
sys forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u0

transpSys :: (HasBuiltins m, MonadError TCErr m, MonadReduce m) =>
               NamesT m (Abs Type) -- ty
               -> [(NamesT m Term, NamesT m Term)] -- sys
               -> NamesT m Term -- φ
               -> NamesT m Term
               -> NamesT m Term
transpSys :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadReduce m) =>
NamesT m (Abs Type)
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
transpSys NamesT m (Abs Type)
ty [(NamesT m Term, NamesT m Term)]
sys NamesT m Term
phi NamesT m Term
u = do
  let max :: NamesT m Term -> NamesT m Term -> NamesT m Term
max NamesT m Term
i NamesT m Term
j = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
j
  Term
iz <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
  Term
tTransp <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans
  Term
tComp <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getTerm' [Char]
builtinComp
  Abs (Level' Term, Term)
l_ty <- forall (m :: * -> *) a.
MonadFail m =>
[Char]
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m (Abs a)
bind [Char]
"i" forall a b. (a -> b) -> a -> b
$ \ forall b. (Subst b, DeBruijn b) => NamesT m b
i -> do
      Type
ty <- forall a. Subst a => Abs a -> SubstArg a -> a
absApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m (Abs Type)
ty forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall b. (Subst b, DeBruijn b) => NamesT m b
i
      forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
toLType Type
ty forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just (LEl Level' Term
l Term
ty) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Level' Term
l,Term
ty)
        Maybe LType
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => Level' Term
__DUMMY_LEVEL__, forall t a. Type'' t a -> a
unEl Type
ty) -- TODO: properly support Setω
  NamesT m Term
l <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Level' Term -> Term
Level forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ Abs (Level' Term, Term)
l_ty
  NamesT m Term
ty <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ Abs (Level' Term, Term)
l_ty

  if forall a. Null a => a -> Bool
null [(NamesT m Term, NamesT m Term)]
sys then forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTransp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
ty forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u else do

  let face :: NamesT m Term
face = forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term -> NamesT m Term
max NamesT m Term
phi (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NamesT m Term -> NamesT m Term -> NamesT m Term
max (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ [(NamesT m Term, NamesT m Term)]
sys)
  NamesT m Term
sys <- (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i'" forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
i -> do
    let base :: (NamesT m Term, NamesT m Term)
base = (NamesT m Term
phi, forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
_ -> NamesT m Term
u)
    forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys NamesT m Term
l NamesT m Term
ty forall a b. (a -> b) -> a -> b
$ (NamesT m Term, NamesT m Term)
base forall a. a -> [a] -> [a]
: [(NamesT m Term
phi, NamesT m Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) | (NamesT m Term
phi,NamesT m Term
u) <- [(NamesT m Term, NamesT m Term)]
sys]

  forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
ty forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
face forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
sys forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u

debugClause :: String -> Clause -> TCM ()
debugClause :: [Char] -> Clause -> TCM ()
debugClause [Char]
s Clause
c = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
s Nat
20 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"gamma:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
s Nat
20 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"ps   :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([NamedArg DeBruijnPattern] -> [Elim]
patternsToElims [NamedArg DeBruijnPattern]
ps)
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
s Nat
20 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"type :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Doc
"nothing" forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Maybe (Arg Type)
rhsTy
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
s Nat
20 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"body :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Doc
"nothing" forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Maybe Term
rhs

      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
s Nat
30 forall a b. (a -> b) -> a -> b
$
        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"c:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Clause
c
  where
    gamma :: Telescope
gamma = Clause -> Telescope
clauseTel Clause
c
    ps :: [NamedArg DeBruijnPattern]
ps = Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
c
    rhsTy :: Maybe (Arg Type)
rhsTy = Clause -> Maybe (Arg Type)
clauseType Clause
c
    rhs :: Maybe Term
rhs = Clause -> Maybe Term
clauseBody Clause
c