-- | 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.Substitute.Class (absBody, raise, apply)

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

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

import Agda.TypeChecking.Primitive.Base
  (SigmaKit(..), (-->), 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
  cubical         <- TCMT IO (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption
  inErasedContext <- hasQuantity0 <$> viewTC eQuantity
  case cubical of
    Just Cubical
CFull -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Cubical
CErased | Cubical
wanted Cubical -> Cubical -> Bool
forall a. Eq a => a -> a -> Bool
== Cubical
CErased Bool -> Bool -> Bool
|| Bool
inErasedContext -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe Cubical
_ -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$ [Char]
"Missing option " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
opt [Char] -> [Char] -> [Char]
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 = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
intervalSort (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
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]
""
  t <- TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType TCMT IO Type -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
  return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \case
    [Arg Term
x] -> do
      unview <- ReduceM (IntervalView -> Term)
forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
      view <- intervalView'
      sx <- reduceB' x
      ix <- intervalView (unArg $ ignoreBlocking sx)

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

        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 (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x)
          OTerm Term
t  -> Arg Term -> IntervalView
INeg (ArgInfo -> Term -> Arg Term
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 ix of
        OTerm Term
t -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced MaybeReducedArgs Term
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sx]
        IntervalView
_       -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (IntervalView -> Term
unview (IntervalView -> Term) -> IntervalView -> Term
forall a b. (a -> b) -> a -> b
$ IntervalView -> IntervalView
f IntervalView
ix)
    [Arg Term]
_ -> [Char] -> ReduceM (Reduced MaybeReducedArgs 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]
""
  t <- Names -> NamesT (TCMT IO) Type -> TCMT IO Type
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT (TCMT IO) Type -> TCMT IO Type)
-> NamesT (TCMT IO) Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$
       [Char]
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"φ" NamesT (TCMT IO) Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
φ ->
       [Char]
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) 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" NamesT (TCMT IO) Term
φ (\ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType) NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> NamesT (TCMT IO) 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.
  return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \case
    [Arg Term
x,Arg Term
y] -> do
      sx <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
x
      ix <- intervalView (unArg $ ignoreBlocking sx)
      itisone <- getTerm "primDepIMin" builtinItIsOne
      case ix of
        -- Σ 0 iy is 0, and additionally P is def.eq. to isOneEmpty.
        IntervalView
IZero -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IntervalView -> ReduceM Term
forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
IZero
        -- Σ 1 iy is (iy 1=1).
        IntervalView
IOne  -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
y) ReduceM Term -> ReduceM Term -> ReduceM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> ReduceM Term
forall a. a -> ReduceM a
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:
          sy <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
y
          iy <- intervalView =<< reduce' =<< (pure (unArg $ ignoreBlocking sy) <@> pure itisone)
          case iy of
            -- Σ _ (λ _ → 0) is always 0
            IntervalView
IZero -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IntervalView -> ReduceM Term
forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
IZero
            -- Σ ix (λ _ → 1) only depends on ix
            IntervalView
IOne  -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sx)
            -- Otherwise we're well and truly blocked.
            IntervalView
_     -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced MaybeReducedArgs Term
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ MaybeReducedArgs -> Reduced MaybeReducedArgs Term
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]
_ -> [Char] -> ReduceM (Reduced MaybeReducedArgs 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]
""
  t <- TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType TCMT IO Type -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType TCMT IO Type -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
  return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \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.
      sx <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
x
      ix <- intervalView (unArg $ ignoreBlocking sx)
      case ix of
        IntervalView
ix | IntervalView
ix IntervalView -> IntervalView -> Bool
==% IntervalView
absorber -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IntervalView -> ReduceM Term
forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
absorber
        IntervalView
ix | IntervalView
ix IntervalView -> IntervalView -> Bool
==% IntervalView
unit     -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced MaybeReducedArgs Term
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Simplification -> Term -> Reduced MaybeReducedArgs Term
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
YesSimplification (Arg Term -> Term
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.
          sy <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
y
          iy <- intervalView (unArg $ ignoreBlocking sy)
          case iy of
            IntervalView
iy | IntervalView
iy IntervalView -> IntervalView -> Bool
==% IntervalView
absorber -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IntervalView -> ReduceM Term
forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
absorber
            IntervalView
iy | IntervalView
iy IntervalView -> IntervalView -> Bool
==% IntervalView
unit     -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced MaybeReducedArgs Term
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Simplification -> Term -> Reduced MaybeReducedArgs Term
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
YesSimplification (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x)
            IntervalView
_                    -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced MaybeReducedArgs Term
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ MaybeReducedArgs -> Reduced MaybeReducedArgs Term
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]
_ -> [Char] -> ReduceM (Reduced MaybeReducedArgs 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
  x' <- m Term
x
  y' <- y
  intervalUnview (IMax (argN x') (argN 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
  x' <- m Term
x
  y' <- y
  intervalUnview (IMin (argN x') (argN 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
  x' <- m Term
x
  intervalUnview (INeg (argN x'))

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

-- | The built-in name associated with a particular Kan operation.
kanOpName :: KanOperation -> String
kanOpName :: KanOperation -> [Char]
kanOpName TranspOp{} = PrimitiveId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
PrimTrans
kanOpName HCompOp{}  = PrimitiveId -> [Char]
forall a. IsBuiltin a => a -> [Char]
getBuiltinId PrimitiveId
PrimHComp

-- | 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
(FamilyOrNot a -> FamilyOrNot a -> Bool)
-> (FamilyOrNot a -> FamilyOrNot a -> Bool) -> Eq (FamilyOrNot a)
forall a. Eq a => FamilyOrNot a -> FamilyOrNot a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: FamilyOrNot a -> FamilyOrNot a -> Bool
Eq,Arity -> FamilyOrNot a -> [Char] -> [Char]
[FamilyOrNot a] -> [Char] -> [Char]
FamilyOrNot a -> [Char]
(Arity -> FamilyOrNot a -> [Char] -> [Char])
-> (FamilyOrNot a -> [Char])
-> ([FamilyOrNot a] -> [Char] -> [Char])
-> Show (FamilyOrNot a)
forall a. Show a => Arity -> FamilyOrNot a -> [Char] -> [Char]
forall a. Show a => [FamilyOrNot a] -> [Char] -> [Char]
forall a. Show a => FamilyOrNot a -> [Char]
forall a.
(Arity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: forall a. Show a => Arity -> FamilyOrNot a -> [Char] -> [Char]
showsPrec :: Arity -> FamilyOrNot a -> [Char] -> [Char]
$cshow :: forall a. Show a => FamilyOrNot a -> [Char]
show :: FamilyOrNot a -> [Char]
$cshowList :: forall a. Show a => [FamilyOrNot a] -> [Char] -> [Char]
showList :: [FamilyOrNot a] -> [Char] -> [Char]
Show,(forall a b. (a -> b) -> FamilyOrNot a -> FamilyOrNot b)
-> (forall a b. a -> FamilyOrNot b -> FamilyOrNot a)
-> Functor FamilyOrNot
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
$cfmap :: forall a b. (a -> b) -> FamilyOrNot a -> FamilyOrNot b
fmap :: forall a b. (a -> b) -> FamilyOrNot a -> FamilyOrNot b
$c<$ :: forall a b. a -> FamilyOrNot b -> FamilyOrNot a
<$ :: forall a b. a -> FamilyOrNot b -> FamilyOrNot a
Functor,(forall m. Monoid m => FamilyOrNot m -> m)
-> (forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m)
-> (forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m)
-> (forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b)
-> (forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b)
-> (forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b)
-> (forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b)
-> (forall a. (a -> a -> a) -> FamilyOrNot a -> a)
-> (forall a. (a -> a -> a) -> FamilyOrNot a -> a)
-> (forall a. FamilyOrNot a -> [a])
-> (forall a. FamilyOrNot a -> Bool)
-> (forall a. FamilyOrNot a -> Arity)
-> (forall a. Eq a => a -> FamilyOrNot a -> Bool)
-> (forall a. Ord a => FamilyOrNot a -> a)
-> (forall a. Ord a => FamilyOrNot a -> a)
-> (forall a. Num a => FamilyOrNot a -> a)
-> (forall a. Num a => FamilyOrNot a -> a)
-> Foldable FamilyOrNot
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
$cfold :: forall m. Monoid m => FamilyOrNot m -> m
fold :: forall m. Monoid m => FamilyOrNot m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> FamilyOrNot a -> a
foldr1 :: forall a. (a -> a -> a) -> FamilyOrNot a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FamilyOrNot a -> a
foldl1 :: forall a. (a -> a -> a) -> FamilyOrNot a -> a
$ctoList :: forall a. FamilyOrNot a -> [a]
toList :: forall a. FamilyOrNot a -> [a]
$cnull :: forall a. FamilyOrNot a -> Bool
null :: forall a. FamilyOrNot a -> Bool
$clength :: forall a. FamilyOrNot a -> Arity
length :: forall a. FamilyOrNot a -> Arity
$celem :: forall a. Eq a => a -> FamilyOrNot a -> Bool
elem :: forall a. Eq a => a -> FamilyOrNot a -> Bool
$cmaximum :: forall a. Ord a => FamilyOrNot a -> a
maximum :: forall a. Ord a => FamilyOrNot a -> a
$cminimum :: forall a. Ord a => FamilyOrNot a -> a
minimum :: forall a. Ord a => FamilyOrNot a -> a
$csum :: forall a. Num a => FamilyOrNot a -> a
sum :: forall a. Num a => FamilyOrNot a -> a
$cproduct :: forall a. Num a => FamilyOrNot a -> a
product :: forall a. Num a => FamilyOrNot a -> a
Foldable,Functor FamilyOrNot
Foldable FamilyOrNot
(Functor FamilyOrNot, Foldable FamilyOrNot) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b))
-> (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 (m :: * -> *) a.
    Monad m =>
    FamilyOrNot (m a) -> m (FamilyOrNot a))
-> Traversable 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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
FamilyOrNot (f a) -> f (FamilyOrNot a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
FamilyOrNot (f a) -> f (FamilyOrNot a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
FamilyOrNot (m a) -> m (FamilyOrNot a)
sequence :: forall (m :: * -> *) a.
Monad m =>
FamilyOrNot (m a) -> m (FamilyOrNot a)
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 = (Blocked' Term a -> Blocked' Term a)
-> FamilyOrNot (Blocked' Term a) -> Blocked (FamilyOrNot a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
traverse Blocked' Term a -> Blocked' Term a
forall a. a -> a
id (FamilyOrNot (Blocked' Term a) -> Blocked (FamilyOrNot a))
-> ReduceM (FamilyOrNot (Blocked' Term a))
-> ReduceM (Blocked (FamilyOrNot a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> ReduceM (Blocked' Term a))
-> FamilyOrNot a -> ReduceM (FamilyOrNot (Blocked' Term a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
traverse a -> ReduceM (Blocked' Term a)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' FamilyOrNot a
x
  reduce' :: FamilyOrNot a -> ReduceM (FamilyOrNot a)
reduce' FamilyOrNot a
x = (a -> ReduceM a) -> FamilyOrNot a -> ReduceM (FamilyOrNot a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
traverse a -> ReduceM a
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@.
-- (See @headStop@ below.)
data TermPosition
  = Head
  | Eliminated
  deriving (TermPosition -> TermPosition -> Bool
(TermPosition -> TermPosition -> Bool)
-> (TermPosition -> TermPosition -> Bool) -> Eq TermPosition
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TermPosition -> TermPosition -> Bool
== :: TermPosition -> TermPosition -> Bool
$c/= :: TermPosition -> TermPosition -> Bool
/= :: TermPosition -> TermPosition -> Bool
Eq,Arity -> TermPosition -> [Char] -> [Char]
[TermPosition] -> [Char] -> [Char]
TermPosition -> [Char]
(Arity -> TermPosition -> [Char] -> [Char])
-> (TermPosition -> [Char])
-> ([TermPosition] -> [Char] -> [Char])
-> Show TermPosition
forall a.
(Arity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Arity -> TermPosition -> [Char] -> [Char]
showsPrec :: Arity -> TermPosition -> [Char] -> [Char]
$cshow :: TermPosition -> [Char]
show :: TermPosition -> [Char]
$cshowList :: [TermPosition] -> [Char] -> [Char]
showList :: [TermPosition] -> [Char] -> [Char]
Show)

-- | Kan operations for the "unstable" type formers (@Glue@, @hcomp {Type}@) are
-- computed "negatively": they never actually produce a @glue φ t a@ term. Instead,
-- we block the computation unless such a term would reduce further, which happens
-- in two cases:
--
-- * when the formula @φ@ is i1, in which case we reduce to @t@;
-- * when we're under an @unglue@, i.e. in 'Eliminated' 'TermPosition', in which case
--   we reduce to @a@.
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
    phi <- Term -> m IntervalView
forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView (Term -> m IntervalView) -> m Term -> m IntervalView
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> m Term) -> m Term -> m Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Term
phi)
    return $ not $ isIOne phi
  | Bool
otherwise = Bool -> m Bool
forall a. a -> m a
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 = (Term, Term) -> Term
forall a b. (a, b) -> b
snd ((Term, Term) -> Term) -> NamesT m (Term, Term) -> NamesT m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m (Term, Term)
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
  tPOr <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> NamesT m (Maybe Term) -> NamesT m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrimitiveId -> NamesT m (Maybe Term)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe Term)
getTerm' PrimitiveId
builtinPOr
  tMax <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIMax
  iz <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIZero
  tEmpty <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIsOneEmpty

  let
    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 = Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tPOr
      NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
l NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
phi NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
psi NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\ NamesT m Term
_ -> NamesT m Term
ty)
      NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u0 NamesT m Term -> NamesT m Term -> NamesT m Term
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 [] = (Term
iz,) (Term -> (Term, Term)) -> NamesT m Term -> NamesT m (Term, Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tEmpty NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
l NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\ NamesT m Term
_ -> NamesT m Term
ty))
    combine [(NamesT m Term
psi, NamesT m Term
u)] = (,) (Term -> Term -> (Term, Term))
-> NamesT m Term -> NamesT m (Term -> (Term, Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT m Term
psi NamesT m (Term -> (Term, Term))
-> NamesT m Term -> NamesT m (Term, Term)
forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
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
      (phi, c) <- [(NamesT m Term, NamesT m Term)] -> NamesT m (Term, Term)
combine [(NamesT m Term, NamesT m Term)]
xs
      (,) <$> imax psi (pure phi) <*> pOr l ty psi (pure phi) u (pure c)
  combine 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
  tPath <- [Char] -> BuiltinId -> NamesT m Term
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
[Char] -> a -> m Term
getTerm [Char]
"fiber" BuiltinId
builtinPath
  kit <- fromMaybe __IMPOSSIBLE__ <$> getSigmaKit
  pure (Def (sigmaName kit) [])
    <#> la <#> lb
    <@> bA
    <@> lam "a" (\ NamesT m Term
a -> Term -> NamesT m Term
forall a. a -> NamesT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tPath NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
lb NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bB NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
f NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
a) NamesT m Term -> NamesT m Term -> NamesT m Term
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
  tHComp <- [Char] -> PrimitiveId -> NamesT m Term
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
[Char] -> a -> m Term
getTerm [Char]
"hfill" PrimitiveId
builtinHComp
  pure tHComp <#> la <#> bA <#> (imax phi (ineg i))
    <@> lam "j" (\ NamesT m Term
j -> NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys NamesT m Term
la NamesT m Term
bA
        [ (NamesT m Term
phi,    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
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 NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imin NamesT m Term
i NamesT m Term
j) NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o))
        , (NamesT m Term -> NamesT m Term
forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
i, [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" (\NamesT m Term
_ -> NamesT m Term
u0))
        ])
    <@> u0

{-# SPECIALIZE decomposeInterval :: Term -> TCM [(IntMap Bool, [Term])] #-}
-- | 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
  Term -> m [(IntMap BoolSet, [Term])]
forall (m :: * -> *).
HasBuiltins m =>
Term -> m [(IntMap BoolSet, [Term])]
decomposeInterval' Term
t m [(IntMap BoolSet, [Term])]
-> ([(IntMap BoolSet, [Term])] -> [(IntMap Bool, [Term])])
-> m [(IntMap Bool, [Term])]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \[(IntMap BoolSet, [Term])]
xs ->
    [ (IntMap Bool
bm, [Term]
ts) | (IntMap BoolSet
bsm, [Term]
ts) <- [(IntMap BoolSet, [Term])]
xs, IntMap Bool
bm <- Maybe (IntMap Bool) -> [IntMap Bool]
forall a. Maybe a -> [a]
maybeToList (Maybe (IntMap Bool) -> [IntMap Bool])
-> Maybe (IntMap Bool) -> [IntMap Bool]
forall a b. (a -> b) -> a -> b
$ (BoolSet -> Maybe Bool) -> IntMap BoolSet -> Maybe (IntMap Bool)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> IntMap a -> f (IntMap b)
traverse BoolSet -> Maybe Bool
BoolSet.toSingleton IntMap BoolSet
bsm ]

{-# SPECIALIZE decomposeInterval' :: Term -> TCM [(IntMap BoolSet, [Term])] #-}
-- | 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
  view   <- m (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  unview <- intervalUnview'
  let
    f :: IntervalView -> [[Either (Int,Bool) Term]]
    -- TODO handle primIMinDep
    -- TODO? handle forall
    f IntervalView
IZero = [[Either (Arity, Bool) Term]]
forall a. [a]
forall (m :: * -> *) a. MonadPlus m => m a
mzero     -- No assignments are possible
    f IntervalView
IOne  = [Either (Arity, Bool) Term] -> [[Either (Arity, Bool) Term]]
forall a. a -> [a]
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
      xs <- (IntervalView -> [[Either (Arity, Bool) Term]]
f (IntervalView -> [[Either (Arity, Bool) Term]])
-> (Arg Term -> IntervalView)
-> Arg Term
-> [[Either (Arity, Bool) Term]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> IntervalView
view (Term -> IntervalView)
-> (Arg Term -> Term) -> Arg Term -> IntervalView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) Arg Term
x
      ys <- (f . view . unArg) y
      return (xs ++ ys)
    -- Take the union
    f (IMax Arg Term
x Arg Term
y) = [[[Either (Arity, Bool) Term]]] -> [[Either (Arity, Bool) Term]]
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([[[Either (Arity, Bool) Term]]] -> [[Either (Arity, Bool) Term]])
-> [[[Either (Arity, Bool) Term]]] -> [[Either (Arity, Bool) Term]]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> [[Either (Arity, Bool) Term]])
-> [Arg Term] -> [[[Either (Arity, Bool) Term]]]
forall a b. (a -> b) -> [a] -> [b]
map (IntervalView -> [[Either (Arity, Bool) Term]]
f (IntervalView -> [[Either (Arity, Bool) Term]])
-> (Arg Term -> IntervalView)
-> Arg Term
-> [[Either (Arity, Bool) Term]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> IntervalView
view (Term -> IntervalView)
-> (Arg Term -> Term) -> Arg Term -> IntervalView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
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) =
      (Either (Arity, Bool) Term -> Either (Arity, Bool) Term)
-> [Either (Arity, Bool) Term] -> [Either (Arity, Bool) Term]
forall a b. (a -> b) -> [a] -> [b]
map (((Arity, Bool) -> Either (Arity, Bool) Term)
-> (Term -> Either (Arity, Bool) Term)
-> Either (Arity, Bool) Term
-> Either (Arity, Bool) Term
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\ (Arity
x,Bool
y) -> (Arity, Bool) -> Either (Arity, Bool) Term
forall a b. a -> Either a b
Left (Arity
x,Bool -> Bool
not Bool
y)) (Term -> Either (Arity, Bool) Term
forall a b. b -> Either a b
Right (Term -> Either (Arity, Bool) Term)
-> (Term -> Term) -> Term -> Either (Arity, Bool) Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntervalView -> Term
unview (IntervalView -> Term) -> (Term -> IntervalView) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> IntervalView
INeg (Arg Term -> IntervalView)
-> (Term -> Arg Term) -> Term -> IntervalView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Arg Term
forall e. e -> Arg e
argN))
        ([Either (Arity, Bool) Term] -> [Either (Arity, Bool) Term])
-> [[Either (Arity, Bool) Term]] -> [[Either (Arity, Bool) Term]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (IntervalView -> [[Either (Arity, Bool) Term]]
f (IntervalView -> [[Either (Arity, Bool) Term]])
-> (Arg Term -> IntervalView)
-> Arg Term
-> [[Either (Arity, Bool) Term]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> IntervalView
view (Term -> IntervalView)
-> (Arg Term -> Term) -> Arg Term -> IntervalView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) Arg Term
x
    f (OTerm (Var Arity
i [])) = [Either (Arity, Bool) Term] -> [[Either (Arity, Bool) Term]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Arity, Bool) -> Either (Arity, Bool) Term
forall a b. a -> Either a b
Left (Arity
i,Bool
True)]
    f (OTerm Term
t)          = [Either (Arity, Bool) Term] -> [[Either (Arity, Bool) Term]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [Term -> Either (Arity, Bool) Term
forall a b. b -> Either a b
Right Term
t]

  return [ (bsm, ts)
         | xs <- f (view t)
         , let (bs,ts) = partitionEithers xs
         , let bsm     = (BoolSet -> BoolSet -> BoolSet)
-> [(Arity, BoolSet)] -> IntMap BoolSet
forall a. (a -> a -> a) -> [(Arity, a)] -> IntMap a
IntMap.fromListWith BoolSet -> BoolSet -> BoolSet
BoolSet.union ([(Arity, BoolSet)] -> IntMap BoolSet)
-> [(Arity, BoolSet)] -> IntMap BoolSet
forall a b. (a -> b) -> a -> b
$ ((Arity, Bool) -> (Arity, BoolSet))
-> [(Arity, Bool)] -> [(Arity, BoolSet)]
forall a b. (a -> b) -> [a] -> [b]
map ((Bool -> BoolSet) -> (Arity, Bool) -> (Arity, BoolSet)
forall b c a. (b -> c) -> (a, b) -> (a, c)
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
  t <- Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
t
  case lam2Abs Relevant t of
    Abs Term
t -> Abs Term
-> (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs Term
t ((Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term))
-> (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term)
forall a b. (a -> b) -> a -> b
$ \ Term
t -> do
      t <- Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
t
      case lam2Abs Irrelevant t of
        Abs Term
t -> Abs Term
-> (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs Term
t Term -> ReduceM (Blocked Term)
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB'
  where
    lam2Abs :: Relevance -> Term -> Abs Term
lam2Abs Relevance
rel (Lam ArgInfo
_ Abs Term
t) = Abs Term -> Term
forall a. Subst a => Abs a -> a
absBody Abs Term
t Term -> Abs Term -> Abs Term
forall a b. a -> Abs b -> Abs a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Abs Term
t
    lam2Abs Relevance
rel Term
t         = [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
Abs [Char]
"y" (Arity -> Term -> Term
forall a. Subst a => Arity -> a -> a
raise Arity
1 Term
t Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Relevance -> Arg Term -> Arg Term
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
rel (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall e. e -> Arg e
argN (Term -> Arg Term) -> Term -> Arg Term
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
  t <- Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
  msub <- getBuiltinName' builtinSub
  case unEl t of
    Def QName
q Elims
es | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
msub, Just (Arg Term
level:Arg Term
typ:Arg Term
phi:Arg Term
ext:[Arg Term]
_) <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
      Maybe (Term, Term, Term, Term)
-> m (Maybe (Term, Term, Term, Term))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Term, Term, Term, Term) -> Maybe (Term, Term, Term, Term)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
level, Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
typ, Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
phi, Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
ext))
    Term
_ -> Maybe (Term, Term, Term, Term)
-> m (Maybe (Term, Term, Term, Term))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term, Term, Term, Term)
forall a. Maybe a
Nothing