-- | Implementations of the basic primitives of Cubical Agda: The
-- interval and its operations.
module Agda.TypeChecking.Primitive.Cubical.Base
  ( requireCubical
  , primIntervalType
  , primIMin', primIMax', primDepIMin', primINeg'
  , imax, imin, ineg

  , Command(..), KanOperation(..), kanOpName, TermPosition(..), headStop
  , FamilyOrNot(..), familyOrNot

    -- * Helper functions for building terms
  , combineSys, combineSys'
  , fiber, hfill
  , decomposeInterval', decomposeInterval
  , reduce2Lam
  , isCubicalSubtype
  )
  where

import Control.Monad        ( msum, mzero )
import Control.Monad.Except ( MonadError )

import qualified Data.IntMap as IntMap
import Data.IntMap (IntMap)
import Data.String (IsString (fromString))
import Data.Bifunctor (second)
import Data.Either (partitionEithers)
import Data.Maybe (fromMaybe, maybeToList)

import qualified Agda.Utils.BoolSet as BoolSet
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.BoolSet (BoolSet)
import Agda.Utils.Functor

import Agda.TypeChecking.Monad.Signature (HasConstInfo)
import Agda.TypeChecking.Monad.Debug (__IMPOSSIBLE_VERBOSE__)
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Pure
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Env

import Agda.TypeChecking.Substitute.Class (absBody, raise, apply)

import Agda.TypeChecking.Reduce (Reduce(..), reduceB', reduce', reduce)
import Agda.TypeChecking.Names (NamesT, runNamesT, ilam, lam)

import Agda.Interaction.Options.Base (optCubical)

import Agda.Syntax.Common
  (Cubical(..), Arg(..), Relevance(..), setRelevance, defaultArgInfo, hasQuantity0)

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

import Agda.Syntax.Internal


-- | Checks that the correct variant of Cubical Agda is activated.
-- Note that @--erased-cubical@ \"counts as\" @--cubical@ in erased
-- contexts.
requireCubical
  :: Cubical -- ^ Which variant of Cubical Agda is required?
  -> String  -- ^ Why, exactly, do we need Cubical to be enabled?
  -> TCM ()
requireCubical :: Cubical -> [Char] -> TCM ()
requireCubical Cubical
wanted [Char]
s = do
  Maybe Cubical
cubical         <- PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  Bool
inErasedContext <- forall a. LensQuantity a => a -> Bool
hasQuantity0 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM TCEnv
getEnv
  case Maybe Cubical
cubical of
    Just Cubical
CFull -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Cubical
CErased | Cubical
wanted forall a. Eq a => a -> a -> Bool
== Cubical
CErased Bool -> Bool -> Bool
|| Bool
inErasedContext -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe Cubical
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"Missing option " forall a. [a] -> [a] -> [a]
++ [Char]
opt forall a. [a] -> [a] -> [a]
++ [Char]
s
  where
  opt :: [Char]
opt = case Cubical
wanted of
    Cubical
CFull   -> [Char]
"--cubical"
    Cubical
CErased -> [Char]
"--cubical or --erased-cubical"

-- | Our good friend the interval type.
primIntervalType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Type
primIntervalType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType = forall t a. Sort' t -> a -> Type'' t a
El Sort
intervalSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInterval

-- | Negation on the interval. Negation satisfies De Morgan's laws, and
-- their implementation is handled here.
primINeg' :: TCM PrimitiveImpl
primINeg' :: TCM PrimitiveImpl
primINeg' = 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 :: * -> *) 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
-> Arity
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
1 forall a b. (a -> b) -> a -> b
$ \case
    [Arg Term
x] -> do
      IntervalView -> Term
unview <- forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
      Term -> IntervalView
view <- forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
      Blocked (Arg Term)
sx <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
x
      IntervalView
ix <- forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView (forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sx)

      -- Apply De Morgan's laws.
      let
        ineg :: Arg Term -> Arg Term
        ineg :: Arg Term -> Arg Term
ineg = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IntervalView -> Term
unview forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntervalView -> IntervalView
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> IntervalView
view)

        f :: IntervalView -> IntervalView
f IntervalView
ix = case IntervalView
ix of
          IntervalView
IZero    -> IntervalView
IOne
          IntervalView
IOne     -> IntervalView
IZero
          IMin Arg Term
x Arg Term
y -> Arg Term -> Arg Term -> IntervalView
IMax (Arg Term -> Arg Term
ineg Arg Term
x) (Arg Term -> Arg Term
ineg Arg Term
y)
          IMax Arg Term
x Arg Term
y -> Arg Term -> Arg Term -> IntervalView
IMin (Arg Term -> Arg Term
ineg Arg Term
x) (Arg Term -> Arg Term
ineg Arg Term
y)
          INeg Arg Term
x   -> Term -> IntervalView
OTerm (forall e. Arg e -> e
unArg Arg Term
x)
          OTerm Term
t  -> Arg Term -> IntervalView
INeg (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo Term
t)

      -- We force the argument in case it happens to be an interval
      -- expression, but it's quite possible that it's _not_. In those
      -- cases, negation is stuck.
      case IntervalView
ix of
        OTerm Term
t -> 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)
sx]
        IntervalView
_       -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn (IntervalView -> Term
unview forall a b. (a -> b) -> a -> b
$ IntervalView -> IntervalView
f IntervalView
ix)
    [Arg Term]
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
"implementation of primINeg called with wrong arity"

-- | 'primDepIMin' expresses that cofibrations are closed under @Σ@.
-- Thus, it serves as a dependent version of 'primIMin' (which, recall,
-- implements @_∧_@). This is required for the construction of the Kan
-- operations in @Id@.
primDepIMin' :: TCM PrimitiveImpl
primDepIMin' :: TCM PrimitiveImpl
primDepIMin' = 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
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 :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
φ (\ NamesT (TCMT IO) Term
o -> forall (m :: * -> *).
(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
  -- Note that the type here is @(φ : I) → (.(IsOne φ) → I) → I@, since
  -- @Partial φ I@ is not well-sorted.
  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
-> Arity
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
2 forall a b. (a -> b) -> a -> b
$ \case
    [Arg Term
x,Arg Term
y] -> do
      Blocked (Arg Term)
sx <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
x
      IntervalView
ix <- forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView (forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sx)
      Term
itisone <- forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm [Char]
"primDepIMin" [Char]
builtinItIsOne
      case IntervalView
ix of
        -- Σ 0 iy is 0, and additionally P is def.eq. to isOneEmpty.
        IntervalView
IZero -> 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 => IntervalView -> m Term
intervalUnview IntervalView
IZero
        -- Σ 1 iy is (iy 1=1).
        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 (f :: * -> *) a. Applicative f => a -> f a
pure (forall e. Arg e -> e
unArg Arg Term
y) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
itisone)
        IntervalView
_     -> do
          -- Hack: We cross our fingers and really hope that eventually
          -- ix may turn out to be i1. Regardless we evaluate iy 1=1, to
          -- short-circuit evaluate a couple of cases:
          Blocked (Arg Term)
sy <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
y
          IntervalView
iy <- forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t. Reduce t => t -> ReduceM t
reduce' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sy) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
itisone)
          case IntervalView
iy of
            -- Σ _ (λ _ → 0) is always 0
            IntervalView
IZero -> 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 => IntervalView -> m Term
intervalUnview IntervalView
IZero
            -- Σ ix (λ _ → 1) only depends on ix
            IntervalView
IOne  -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn (forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sx)
            -- Otherwise we're well and truly blocked.
            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 [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sx, Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sy]
    [Arg Term]
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
"implementation of primDepIMin called with wrong arity"

-- | Internal helper for constructing binary operations on the interval,
-- parameterised by their unit and absorbing elements.
primIBin :: IntervalView -> IntervalView -> TCM PrimitiveImpl
primIBin :: IntervalView -> IntervalView -> TCM PrimitiveImpl
primIBin IntervalView
unit IntervalView
absorber = 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
-> Arity
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
2 forall a b. (a -> b) -> a -> b
$ \case
    [Arg Term
x,Arg Term
y] -> do
      -- Evaluation here is short-circuiting: If the LHS is either the
      -- absorbing or unit element, then the RHS does not matter.
      Blocked (Arg Term)
sx <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
x
      IntervalView
ix <- forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView (forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sx)
      case IntervalView
ix of
        IntervalView
ix | IntervalView
ix IntervalView -> IntervalView -> Bool
==% IntervalView
absorber -> 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 => IntervalView -> m Term
intervalUnview IntervalView
absorber
        IntervalView
ix | IntervalView
ix IntervalView -> IntervalView -> Bool
==% IntervalView
unit     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
YesSimplification (forall e. Arg e -> e
unArg Arg Term
y)
        IntervalView
_ -> do
          -- And in the case where the LHS is stuck, we can make
          -- progress by comparing the LHS to the absorbing/unit
          -- elements.
          Blocked (Arg Term)
sy <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
y
          IntervalView
iy <- forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView (forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sy)
          case IntervalView
iy of
            IntervalView
iy | IntervalView
iy IntervalView -> IntervalView -> Bool
==% IntervalView
absorber -> 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 => IntervalView -> m Term
intervalUnview IntervalView
absorber
            IntervalView
iy | IntervalView
iy IntervalView -> IntervalView -> Bool
==% IntervalView
unit     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
YesSimplification (forall e. Arg e -> e
unArg Arg Term
x)
            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 [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sx,Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sy]
    [Arg Term]
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
"binary operation on the interval called with incorrect arity"
  where
    ==% :: IntervalView -> IntervalView -> Bool
(==%) IntervalView
IZero IntervalView
IZero = Bool
True
    (==%) IntervalView
IOne IntervalView
IOne = Bool
True
    (==%) IntervalView
_ IntervalView
_ = Bool
False
{-# INLINE primIBin #-}

-- | Implements both the @min@ connection /and/ conjunction on the
-- cofibration classifier.
primIMin' :: TCM PrimitiveImpl
primIMin' :: TCM PrimitiveImpl
primIMin' = do
  Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
  IntervalView -> IntervalView -> TCM PrimitiveImpl
primIBin IntervalView
IOne IntervalView
IZero

-- | Implements both the @max@ connection /and/ disjunction on the
-- cofibration classifier.
primIMax' :: TCM PrimitiveImpl
primIMax' :: TCM PrimitiveImpl
primIMax' = do
  Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
  IntervalView -> IntervalView -> TCM PrimitiveImpl
primIBin IntervalView
IZero IntervalView
IOne

-- | A helper for evaluating @max@ on the interval in TCM&co.
imax :: HasBuiltins m => m Term -> m Term -> m Term
imax :: forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax m Term
x m Term
y = do
  Term
x' <- m Term
x
  Term
y' <- m Term
y
  forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview (Arg Term -> Arg Term -> IntervalView
IMax (forall e. e -> Arg e
argN Term
x') (forall e. e -> Arg e
argN Term
y'))

-- | A helper for evaluating @min@ on the interval in TCM&co.
imin :: HasBuiltins m => m Term -> m Term -> m Term
imin :: forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imin m Term
x m Term
y = do
  Term
x' <- m Term
x
  Term
y' <- m Term
y
  forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview (Arg Term -> Arg Term -> IntervalView
IMin (forall e. e -> Arg e
argN Term
x') (forall e. e -> Arg e
argN Term
y'))

-- | A helper for evaluating @neg@ on the interval in TCM&co.
ineg :: HasBuiltins m => m Term -> m Term
ineg :: forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg m Term
x = do
  Term
x' <- m Term
x
  forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview (Arg Term -> IntervalView
INeg (forall e. e -> Arg e
argN Term
x'))

data Command = DoTransp | DoHComp
  deriving (Command -> Command -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Command -> Command -> Bool
$c/= :: Command -> Command -> Bool
== :: Command -> Command -> Bool
$c== :: Command -> Command -> Bool
Eq, Arity -> Command -> ShowS
[Command] -> ShowS
Command -> [Char]
forall a.
(Arity -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Command] -> ShowS
$cshowList :: [Command] -> ShowS
show :: Command -> [Char]
$cshow :: Command -> [Char]
showsPrec :: Arity -> Command -> ShowS
$cshowsPrec :: Arity -> Command -> ShowS
Show)

-- | The built-in name associated with a particular Kan operation.
kanOpName :: KanOperation -> String
kanOpName :: KanOperation -> [Char]
kanOpName TranspOp{} = [Char]
builtinTrans
kanOpName HCompOp{}  = [Char]
builtinHComp

-- | Our Kan operations are @transp@ and @hcomp@. The KanOperation
-- record stores the data associated with a Kan operation on arbitrary
-- types: A cofibration and an element of that type.
data KanOperation
  -- | A transport problem consists of a cofibration, marking where the
  -- transport is constant, and a term to move from the fibre over i0 to
  -- the fibre over i1.
  = TranspOp
    { KanOperation -> Blocked (Arg Term)
kanOpCofib :: Blocked (Arg Term)
      -- ^ When this cofibration holds, the transport must
      -- definitionally be the identity. This is handled generically by
      -- 'primTransHComp' but specific Kan operations may still need it.
    , KanOperation -> Arg Term
kanOpBase :: Arg Term
      -- ^ This is the term in @A i0@ which we are transporting.
    }
  -- | A composition problem consists of a partial element and a base.
  -- Semantically, this is justified by the types being Kan fibrations,
  -- i.e., having the lifting property against trivial cofibrations.
  -- While the specified cofibration may not be trivial, (φ ∨ ~ r) for r
  -- ∉ φ is *always* a trivial cofibration.
  | HCompOp
    { kanOpCofib :: Blocked (Arg Term)
      -- ^ Extent of definition of the partial element we are lifting
      -- against.
    , KanOperation -> Arg Term
kanOpSides :: Arg Term
      -- ^ The partial element itself
    , kanOpBase  :: Arg Term
      -- ^ The base.
    }

-- | Are we looking at a family of things, or at a single thing?
data FamilyOrNot a
  = IsFam { forall a. FamilyOrNot a -> a
famThing :: a }
  | IsNot { famThing :: a }
  deriving (FamilyOrNot a -> FamilyOrNot a -> Bool
forall a. Eq a => FamilyOrNot a -> FamilyOrNot a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FamilyOrNot a -> FamilyOrNot a -> Bool
$c/= :: forall a. Eq a => FamilyOrNot a -> FamilyOrNot a -> Bool
== :: FamilyOrNot a -> FamilyOrNot a -> Bool
$c== :: forall a. Eq a => FamilyOrNot a -> FamilyOrNot a -> Bool
Eq,Arity -> FamilyOrNot a -> ShowS
forall a. Show a => Arity -> FamilyOrNot a -> ShowS
forall a. Show a => [FamilyOrNot a] -> ShowS
forall a. Show a => FamilyOrNot a -> [Char]
forall a.
(Arity -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [FamilyOrNot a] -> ShowS
$cshowList :: forall a. Show a => [FamilyOrNot a] -> ShowS
show :: FamilyOrNot a -> [Char]
$cshow :: forall a. Show a => FamilyOrNot a -> [Char]
showsPrec :: Arity -> FamilyOrNot a -> ShowS
$cshowsPrec :: forall a. Show a => Arity -> FamilyOrNot a -> ShowS
Show,forall a b. a -> FamilyOrNot b -> FamilyOrNot a
forall a b. (a -> b) -> FamilyOrNot a -> FamilyOrNot b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> FamilyOrNot b -> FamilyOrNot a
$c<$ :: forall a b. a -> FamilyOrNot b -> FamilyOrNot a
fmap :: forall a b. (a -> b) -> FamilyOrNot a -> FamilyOrNot b
$cfmap :: forall a b. (a -> b) -> FamilyOrNot a -> FamilyOrNot b
Functor,forall a. Eq a => a -> FamilyOrNot a -> Bool
forall a. Num a => FamilyOrNot a -> a
forall a. Ord a => FamilyOrNot a -> a
forall m. Monoid m => FamilyOrNot m -> m
forall a. FamilyOrNot a -> Bool
forall a. FamilyOrNot a -> Arity
forall a. FamilyOrNot a -> [a]
forall a. (a -> a -> a) -> FamilyOrNot a -> a
forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m
forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b
forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Arity)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => FamilyOrNot a -> a
$cproduct :: forall a. Num a => FamilyOrNot a -> a
sum :: forall a. Num a => FamilyOrNot a -> a
$csum :: forall a. Num a => FamilyOrNot a -> a
minimum :: forall a. Ord a => FamilyOrNot a -> a
$cminimum :: forall a. Ord a => FamilyOrNot a -> a
maximum :: forall a. Ord a => FamilyOrNot a -> a
$cmaximum :: forall a. Ord a => FamilyOrNot a -> a
elem :: forall a. Eq a => a -> FamilyOrNot a -> Bool
$celem :: forall a. Eq a => a -> FamilyOrNot a -> Bool
length :: forall a. FamilyOrNot a -> Arity
$clength :: forall a. FamilyOrNot a -> Arity
null :: forall a. FamilyOrNot a -> Bool
$cnull :: forall a. FamilyOrNot a -> Bool
toList :: forall a. FamilyOrNot a -> [a]
$ctoList :: forall a. FamilyOrNot a -> [a]
foldl1 :: forall a. (a -> a -> a) -> FamilyOrNot a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FamilyOrNot a -> a
foldr1 :: forall a. (a -> a -> a) -> FamilyOrNot a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> FamilyOrNot a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b
foldl :: forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b
foldr :: forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m
fold :: forall m. Monoid m => FamilyOrNot m -> m
$cfold :: forall m. Monoid m => FamilyOrNot m -> m
Foldable,Functor FamilyOrNot
Foldable FamilyOrNot
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
FamilyOrNot (m a) -> m (FamilyOrNot a)
forall (f :: * -> *) a.
Applicative f =>
FamilyOrNot (f a) -> f (FamilyOrNot a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
sequence :: forall (m :: * -> *) a.
Monad m =>
FamilyOrNot (m a) -> m (FamilyOrNot a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
FamilyOrNot (m a) -> m (FamilyOrNot a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
FamilyOrNot (f a) -> f (FamilyOrNot a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
FamilyOrNot (f a) -> f (FamilyOrNot a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
Traversable)

familyOrNot :: IsString p => FamilyOrNot a -> p
familyOrNot :: forall p a. IsString p => FamilyOrNot a -> p
familyOrNot (IsFam a
x) = p
"IsFam"
familyOrNot (IsNot a
x) = p
"IsNot"

instance Reduce a => Reduce (FamilyOrNot a) where
  reduceB' :: FamilyOrNot a -> ReduceM (Blocked (FamilyOrNot a))
reduceB' FamilyOrNot a
x = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. a -> a
id 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 t. Reduce t => t -> ReduceM (Blocked t)
reduceB' FamilyOrNot a
x
  reduce' :: FamilyOrNot a -> ReduceM (FamilyOrNot a)
reduce' FamilyOrNot a
x = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall t. Reduce t => t -> ReduceM t
reduce' FamilyOrNot a
x

-- | For the Kan operations in @Glue@ and @hcomp {Type}@, we optimise
-- evaluation a tiny bit by differentiating the term produced when
-- evaluating a Kan operation by itself vs evaluating it under @unglue@.
data TermPosition
  = Head
  | Eliminated
  deriving (TermPosition -> TermPosition -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TermPosition -> TermPosition -> Bool
$c/= :: TermPosition -> TermPosition -> Bool
== :: TermPosition -> TermPosition -> Bool
$c== :: TermPosition -> TermPosition -> Bool
Eq,Arity -> TermPosition -> ShowS
[TermPosition] -> ShowS
TermPosition -> [Char]
forall a.
(Arity -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TermPosition] -> ShowS
$cshowList :: [TermPosition] -> ShowS
show :: TermPosition -> [Char]
$cshow :: TermPosition -> [Char]
showsPrec :: Arity -> TermPosition -> ShowS
$cshowsPrec :: Arity -> TermPosition -> ShowS
Show)

-- | If we're computing a Kan operation for one of the "unstable" type
-- formers (@Glue@, @hcomp {Type}@), this tells us whether the type will
-- reduce further, and whether we should care.
--
-- When should we care? When we're in the 'Head' 'TermPosition'. When
-- will the type reduce further? When @φ@, its formula, is not i1.
headStop :: PureTCM m => TermPosition -> m Term -> m Bool
headStop :: forall (m :: * -> *). PureTCM m => TermPosition -> m Term -> m Bool
headStop TermPosition
tpos m Term
phi
  | TermPosition
Head <- TermPosition
tpos = do
    IntervalView
phi <- forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Term
phi)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ IntervalView -> Bool
isIOne IntervalView
phi
  | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | Build a partial element. The type of the resulting partial element
-- can depend on the computed extent, which we denote by @φ@ here. Note
-- that @φ@ is the n-ary disjunction of all the @ψ@s.
combineSys
  :: HasBuiltins m
  => NamesT m Term -- The level @l : Level@
  -> NamesT m Term -- The type @A : Partial φ (Type l)@.
  -> [(NamesT m Term, NamesT m Term)]
  -- ^ A list of @(ψ, PartialP ψ λ o → A (... o ...))@ mappings. Note
  -- that by definitional proof-irrelevance of @IsOne@, the actual
  -- injection can not matter here.
  -> NamesT m Term
combineSys :: 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, NamesT m Term)]
xs = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m (Term, Term)
combineSys' NamesT m Term
l NamesT m Term
ty [(NamesT m Term, NamesT m Term)]
xs

-- | Build a partial element, and compute its extent. See 'combineSys'
-- for the details.
combineSys'
  :: forall m. HasBuiltins m
  => NamesT m Term -- The level @l@
  -> NamesT m Term -- The type @A@
  -> [(NamesT m Term, NamesT m Term)]
  -> NamesT m (Term,Term)
combineSys' :: forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m (Term, Term)
combineSys' NamesT m Term
l NamesT m Term
ty [(NamesT m Term, NamesT m Term)]
xs = do
  Term
tPOr <- 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]
builtinPOr
  Term
tMax <- 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]
builtinIMax
  Term
iz <- 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]
builtinIZero
  Term
tEmpty <- 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]
builtinIsOneEmpty

  let
    pOr :: NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
pOr NamesT m Term
l NamesT m Term
ty NamesT m Term
phi NamesT m Term
psi NamesT m Term
u0 NamesT m Term
u1 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tPOr
      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
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
psi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
_ -> NamesT m Term
ty)
      forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u0 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u1

    -- In one pass, compute the disjunction of all the cofibrations and
    -- compute the primPOr expression.
    combine :: [(NamesT m Term, NamesT m Term)] -> NamesT m (Term, Term)
    combine :: [(NamesT m Term, NamesT m Term)] -> NamesT m (Term, Term)
combine [] = (Term
iz,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tEmpty forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m 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" forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
_ -> NamesT m Term
ty))
    combine [(NamesT m Term
psi, NamesT m Term
u)] = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m Term
psi forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT m Term
u
    combine ((NamesT m Term
psi, NamesT m Term
u):[(NamesT m Term, NamesT m Term)]
xs) = do
      (Term
phi, Term
c) <- [(NamesT m Term, NamesT m Term)] -> NamesT m (Term, Term)
combine [(NamesT m Term, NamesT m Term)]
xs
      (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
phi) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
pOr NamesT m Term
l NamesT m Term
ty NamesT m Term
psi (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
phi) NamesT m Term
u (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
c)
  [(NamesT m Term, NamesT m Term)] -> NamesT m (Term, Term)
combine [(NamesT m Term, NamesT m Term)]
xs

-- | Helper function for constructing the type of fibres of a function
-- over a given point.
fiber
  :: (HasBuiltins m, HasConstInfo m)
  => NamesT m Term -- @la : Level@
  -> NamesT m Term -- @lb : Level@
  -> NamesT m Term -- @A : Type la@
  -> NamesT m Term -- @B : Type lb@
  -> NamesT m Term -- @f : A → B@
  -> NamesT m Term -- @x : B@
  -> NamesT m Term -- @Σ[ x ∈ A ] (f a ≡ x)@
fiber :: forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
fiber NamesT m Term
la NamesT m Term
lb NamesT m Term
bA NamesT m Term
bB NamesT m Term
f NamesT m Term
b = do
  Term
tPath <- forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm [Char]
"fiber" [Char]
builtinPath
  SigmaKit
kit <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Elims -> Term
Def (SigmaKit -> QName
sigmaName SigmaKit
kit) [])
    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
lb
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
bA
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"a" (\ NamesT m Term
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tPath forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bB forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
f forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
a) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
b)

-- | Helper function for constructing the filler of a given composition
-- problem.
hfill
  :: (HasBuiltins m, HasConstInfo m)
  => NamesT m Term -- @la : Level@
  -> NamesT m Term -- @A : Type la@
  -> NamesT m Term -- @φ : I@. Cofibration
  -> NamesT m Term -- @u : Partial φ A@.
  -> NamesT m Term -- @u0 : A@. Must agree with @u@ on @φ@
  -> NamesT m Term -- @i : I@. Position along the cube.
  -> NamesT m Term
hfill :: forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
hfill NamesT m Term
la NamesT m Term
bA NamesT m Term
phi NamesT m Term
u NamesT m Term
u0 NamesT m Term
i = do
  Term
tHComp <- forall (m :: * -> *). HasBuiltins m => [Char] -> [Char] -> m Term
getTerm [Char]
"hfill" [Char]
builtinHComp
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
phi (forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
i))
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"j" (\ NamesT m Term
j -> forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys NamesT m Term
la NamesT m Term
bA
        [ (NamesT m Term
phi,    forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\NamesT m Term
o -> NamesT m Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imin NamesT m Term
i NamesT m Term
j) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o))
        , (forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
i, forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\NamesT m Term
_ -> NamesT m Term
u0))
        ])
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u0

-- | Decompose an interval expression @i : I@ as in
-- 'decomposeInterval'', but discard any inconsistent mappings.
decomposeInterval :: HasBuiltins m => Term -> m [(IntMap Bool, [Term])]
decomposeInterval :: forall (m :: * -> *).
HasBuiltins m =>
Term -> m [(IntMap Bool, [Term])]
decomposeInterval Term
t = do
  forall (m :: * -> *).
HasBuiltins m =>
Term -> m [(IntMap BoolSet, [Term])]
decomposeInterval' Term
t forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \[(IntMap BoolSet, [Term])]
xs ->
    [ (IntMap Bool
bm, [Term]
ts) | (IntMap BoolSet
bsm, [Term]
ts) <- [(IntMap BoolSet, [Term])]
xs, IntMap Bool
bm <- forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse BoolSet -> Maybe Bool
BoolSet.toSingleton IntMap BoolSet
bsm ]

-- | Decompose an interval expression @φ : I@ into a set of possible
-- assignments for the variables mentioned in @φ@, together any leftover
-- neutral terms that could not be put into 'IntervalView' form.
decomposeInterval' :: HasBuiltins m => Term -> m [(IntMap BoolSet, [Term])]
decomposeInterval' :: forall (m :: * -> *).
HasBuiltins m =>
Term -> m [(IntMap BoolSet, [Term])]
decomposeInterval' 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'
  let
    f :: IntervalView -> [[Either (Int,Bool) Term]]
    -- TODO handle primIMinDep
    -- TODO? handle forall
    f :: IntervalView -> [[Either (Arity, Bool) Term]]
f IntervalView
IZero = forall (m :: * -> *) a. MonadPlus m => m a
mzero     -- No assignments are possible
    f IntervalView
IOne  = forall (m :: * -> *) a. Monad m => a -> m a
return [] -- No assignments are necessary
    -- Take the cartesian product
    f (IMin Arg Term
x Arg Term
y) = do
      [Either (Arity, Bool) Term]
xs <- (IntervalView -> [[Either (Arity, Bool) Term]]
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> IntervalView
view forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) Arg Term
x
      [Either (Arity, Bool) Term]
ys <- (IntervalView -> [[Either (Arity, Bool) Term]]
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> IntervalView
view forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) Arg Term
y
      forall (m :: * -> *) a. Monad m => a -> m a
return ([Either (Arity, Bool) Term]
xs forall a. [a] -> [a] -> [a]
++ [Either (Arity, Bool) Term]
ys)
    -- Take the union
    f (IMax Arg Term
x Arg Term
y) = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (IntervalView -> [[Either (Arity, Bool) Term]]
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> IntervalView
view forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
x,Arg Term
y]
    -- Invert the possible assignments and negate the neutrals
    f (INeg Arg Term
x) =
      forall a b. (a -> b) -> [a] -> [b]
map (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\ (Arity
x,Bool
y) -> forall a b. a -> Either a b
Left (Arity
x,Bool -> Bool
not Bool
y)) (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntervalView -> Term
unview forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> IntervalView
INeg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. e -> Arg e
argN))
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (IntervalView -> [[Either (Arity, Bool) Term]]
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> IntervalView
view forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) Arg Term
x
    f (OTerm (Var Arity
i [])) = forall (m :: * -> *) a. Monad m => a -> m a
return [forall a b. a -> Either a b
Left (Arity
i,Bool
True)]
    f (OTerm Term
t)          = forall (m :: * -> *) a. Monad m => a -> m a
return [forall a b. b -> Either a b
Right Term
t]

  forall (m :: * -> *) a. Monad m => a -> m a
return [ (IntMap BoolSet
bsm, [Term]
ts)
         | [Either (Arity, Bool) Term]
xs <- IntervalView -> [[Either (Arity, Bool) Term]]
f (Term -> IntervalView
view Term
t)
         , let ([(Arity, Bool)]
bs,[Term]
ts) = forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (Arity, Bool) Term]
xs
         , let bsm :: IntMap BoolSet
bsm     = forall a. (a -> a -> a) -> [(Arity, a)] -> IntMap a
IntMap.fromListWith BoolSet -> BoolSet -> BoolSet
BoolSet.union forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Bool -> BoolSet
BoolSet.singleton) [(Arity, Bool)]
bs
         ]

reduce2Lam :: Term -> ReduceM (Blocked Term)
reduce2Lam :: Term -> ReduceM (Blocked Term)
reduce2Lam Term
t = do
  Term
t <- forall t. Reduce t => t -> ReduceM t
reduce' Term
t
  case Relevance -> Term -> Abs Term
lam2Abs Relevance
Relevant Term
t of
    Abs Term
t -> forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs Term
t forall a b. (a -> b) -> a -> b
$ \ Term
t -> do
      Term
t <- forall t. Reduce t => t -> ReduceM t
reduce' Term
t
      case Relevance -> Term -> Abs Term
lam2Abs Relevance
Irrelevant Term
t of
        Abs Term
t -> forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs Term
t forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB'
  where
    lam2Abs :: Relevance -> Term -> Abs Term
lam2Abs Relevance
rel (Lam ArgInfo
_ Abs Term
t) = forall a. Subst a => Abs a -> a
absBody Abs Term
t forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Abs Term
t
    lam2Abs Relevance
rel Term
t         = forall a. [Char] -> a -> Abs a
Abs [Char]
"y" (forall a. Subst a => Arity -> a -> a
raise Arity
1 Term
t forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
rel forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ Arity -> Term
var Arity
0])

-- | Are we looking at an application of the 'Sub' type? If so, return:
-- * The type we're an extension of
-- * The extent
-- * The partial element.
isCubicalSubtype :: PureTCM m => Type -> m (Maybe (Term, Term, Term, Term))
isCubicalSubtype :: forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (Term, Term, Term, Term))
isCubicalSubtype Type
t = do
  Type
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
  Maybe QName
msub <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinSub
  case forall t a. Type'' t a -> a
unEl Type
t of
    Def QName
q Elims
es | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
msub, Just (Arg Term
level:Arg Term
typ:Arg Term
phi:Arg Term
ext:[Arg Term]
_) <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall e. Arg e -> e
unArg Arg Term
level, forall e. Arg e -> e
unArg Arg Term
typ, forall e. Arg e -> e
unArg Arg Term
phi, forall e. Arg e -> e
unArg Arg Term
ext))
    Term
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing