| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Primitive.Cubical
Synopsis
- type LM m a = NamesT (ExceptT (Closure (Abs Type)) m) a
- data TranspError = CannotTransp {}
- data LType = LEl Level Term
- data CType
- primPOr :: TCM PrimitiveImpl
- primComp :: TCM PrimitiveImpl
- primTransHComp :: Command -> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
- primPartial' :: TCM PrimitiveImpl
- primPartialP' :: TCM PrimitiveImpl
- primSubOut' :: TCM PrimitiveImpl
- primTrans' :: TCM PrimitiveImpl
- primHComp' :: TCM PrimitiveImpl
- mkComp :: HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)
- mkCompLazy :: HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)
- doPiKanOp :: KanOperation -> ArgName -> FamilyOrNot (Dom Type, Abs Type) -> ReduceM (Maybe Term)
- doPathPKanOp :: KanOperation -> FamilyOrNot (Arg Term) -> FamilyOrNot (Arg Term, Arg Term, Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
- redReturnNoSimpl :: a -> ReduceM (Reduced a' a)
- hcomp :: (HasBuiltins m, MonadError TCErr m, MonadReduce m, MonadPretty m) => NamesT m Type -> [(NamesT m Term, NamesT m Term)] -> NamesT m Term -> NamesT m Term
- primFaceForall' :: TCM PrimitiveImpl
- transpTel :: Abs Telescope -> Term -> Args -> ExceptT (Closure (Abs Type)) TCM Args
- transpTel' :: (PureTCM m, MonadError TCErr m) => Bool -> Abs Telescope -> Term -> Args -> ExceptT (Closure (Abs Type)) m Args
- transpSysTel' :: forall m. (PureTCM m, MonadError TCErr m) => Bool -> Abs Telescope -> [(Term, Abs [Term])] -> Term -> Args -> ExceptT (Closure (Abs Type)) m Args
- trFillTel' :: (PureTCM m, MonadError TCErr m) => Bool -> Abs Telescope -> Term -> Args -> Term -> ExceptT (Closure (Abs Type)) m Args
- trFillTel :: Abs Telescope -> Term -> Args -> Term -> ExceptT (Closure (Abs Type)) TCM Args
- pathTelescope :: forall m. (PureTCM m, MonadError TCErr m) => Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
- pathTelescope' :: forall m. (PureTCM m, MonadError (Closure Type) m) => Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
- tryTranspError :: TCM a -> TCM (Either (Closure (Abs Type)) a)
- transpPathPTel' :: NamesT TCM (Abs (Abs Telescope)) -> [NamesT TCM Term] -> [NamesT TCM Term] -> NamesT TCM Term -> [NamesT TCM Term] -> NamesT TCM [Arg Term]
- transpPathTel' :: NamesT TCM (Abs Telescope) -> [NamesT TCM Term] -> [NamesT TCM Term] -> NamesT TCM Term -> [NamesT TCM Term] -> NamesT TCM [Arg Term]
- trFillPathTel' :: NamesT TCM (Abs Telescope) -> [NamesT TCM Term] -> [NamesT TCM Term] -> NamesT TCM Term -> [NamesT TCM Term] -> NamesT TCM Term -> NamesT TCM [Arg Term]
- trFillPathPTel' :: NamesT TCM (Abs (Abs Telescope)) -> [NamesT TCM Term] -> [NamesT TCM Term] -> NamesT TCM Term -> [NamesT TCM Term] -> NamesT TCM Term -> NamesT TCM [Arg Term]
- expTelescope :: Type -> Telescope -> Telescope
- expS :: Nat -> Substitution
- fromLType :: LType -> Type
- lTypeLevel :: LType -> Level
- toLType :: MonadReduce m => Type -> m (Maybe LType)
- fromCType :: CType -> Type
- toCType :: MonadReduce m => Type -> m (Maybe CType)
- transpSys :: (HasBuiltins m, MonadError TCErr m, MonadReduce m) => NamesT m (Abs Type) -> [(NamesT m Term, NamesT m Term)] -> NamesT m Term -> NamesT m Term -> NamesT m Term
- debugClause :: String -> Clause -> TCM ()
- module Agda.TypeChecking.Primitive.Cubical.Id
- module Agda.TypeChecking.Primitive.Cubical.Base
- module Agda.TypeChecking.Primitive.Cubical.Glue
- module Agda.TypeChecking.Primitive.Cubical.HCompU
Documentation
data TranspError Source #
Constructors
| CannotTransp | |
Instances
| Exception TranspError Source # | |
Defined in Agda.TypeChecking.Primitive.Cubical Methods toException :: TranspError -> SomeException # fromException :: SomeException -> Maybe TranspError # displayException :: TranspError -> String # | |
| Show TranspError Source # | |
Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> TranspError -> ShowS # show :: TranspError -> String # showList :: [TranspError] -> ShowS # | |
A Type with sort Type l
Such a type supports both hcomp and transp.
A Type that either has sort Type l or is a closed definition.
Such a type supports some version of transp.
In particular we want to allow the Interval as a ClosedType.
Constructors
| ClosedType Sort QName | |
| LType LType |
mkComp :: HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term) Source #
Construct a helper for CCHM composition, with a string indicating what function uses it.
mkCompLazy :: HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term) Source #
Construct an application of buitlinComp. Use instead of mkComp if
reducing directly to hcomp + transport would be problematic.
Arguments
| :: KanOperation | Are we composing or transporting? |
| -> ArgName | Name of the binder |
| -> FamilyOrNot (Dom Type, Abs Type) | The domain and codomain of the Pi type. |
| -> ReduceM (Maybe Term) |
Implementation of Kan operations for Pi types. The implementation
of transp and hcomp for Pi types has many commonalities, so most
of it is shared between the two cases.
doPathPKanOp :: KanOperation -> FamilyOrNot (Arg Term) -> FamilyOrNot (Arg Term, Arg Term, Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term) Source #
Compute Kan operations in a type of dependent paths.
redReturnNoSimpl :: a -> ReduceM (Reduced a' a) Source #
hcomp :: (HasBuiltins m, MonadError TCErr m, MonadReduce m, MonadPretty m) => NamesT m Type -> [(NamesT m Term, NamesT m Term)] -> NamesT m Term -> NamesT m Term Source #
transpTel :: Abs Telescope -> Term -> Args -> ExceptT (Closure (Abs Type)) TCM Args Source #
Tries to primTransp a whole telescope of arguments, following the rule for Σ types.
If a type in the telescope does not support transp, transpTel throws it as an exception.
transpTel' :: (PureTCM m, MonadError TCErr m) => Bool -> Abs Telescope -> Term -> Args -> ExceptT (Closure (Abs Type)) m Args Source #
transpSysTel' :: forall m. (PureTCM m, MonadError TCErr m) => Bool -> Abs Telescope -> [(Term, Abs [Term])] -> Term -> Args -> ExceptT (Closure (Abs Type)) m Args Source #
trFillTel' :: (PureTCM m, MonadError TCErr m) => Bool -> Abs Telescope -> Term -> Args -> Term -> ExceptT (Closure (Abs Type)) m Args Source #
trFillTel :: Abs Telescope -> Term -> Args -> Term -> ExceptT (Closure (Abs Type)) TCM Args Source #
Like transpTel but performing a transpFill.
pathTelescope :: forall m. (PureTCM m, MonadError TCErr m) => Telescope -> [Arg Term] -> [Arg Term] -> m Telescope Source #
pathTelescope' :: forall m. (PureTCM m, MonadError (Closure Type) m) => Telescope -> [Arg Term] -> [Arg Term] -> m Telescope Source #
expS :: Nat -> Substitution Source #
Γ, Δ^I, i : I |- expS |Δ| : Γ, Δ
lTypeLevel :: LType -> Level Source #