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 {
- errorType :: Closure (Abs Type)
}
data LType = LEl Level Term
data CType
- = ClosedType Sort QName
- | LType LType
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 :: forall m. HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)
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

type LM m a = NamesT (ExceptT (Closure (Abs Type)) m) a Source #

data TranspError Source #

Constructors

CannotTransp
Fields errorType :: Closure (Abs Type)

Instances

Instances details

Exception TranspError Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods toException :: TranspError -> SomeException # fromException :: SomeException -> Maybe TranspError # displayException :: TranspError -> String #
Show TranspError Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> TranspError -> ShowS # show :: TranspError -> String # showList :: [TranspError] -> ShowS #

data LType Source #

A Type with sort Type l Such a type supports both hcomp and transp.

Constructors

LEl Level Term

Instances

Instances details

Subst LType Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Associated Types type SubstArg LType Source # Methods applySubst :: Substitution' (SubstArg LType) -> LType -> LType Source #
Show LType Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> LType -> ShowS # show :: LType -> String # showList :: [LType] -> ShowS #
Eq LType Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods (==) :: LType -> LType -> Bool # (/=) :: LType -> LType -> Bool #
type SubstArg LType Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical type SubstArg LType = Term

data CType Source #

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

Instances

Instances details

Pretty CType Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods pretty :: CType -> Doc Source # prettyPrec :: Int -> CType -> Doc Source # prettyList :: [CType] -> Doc Source #
Subst CType Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Associated Types type SubstArg CType Source # Methods applySubst :: Substitution' (SubstArg CType) -> CType -> CType Source #
Show CType Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> CType -> ShowS # show :: CType -> String # showList :: [CType] -> ShowS #
Eq CType Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods (==) :: CType -> CType -> Bool # (/=) :: CType -> CType -> Bool #
type SubstArg CType Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical type SubstArg CType = Term

primPOr :: TCM PrimitiveImpl Source #

primComp :: TCM PrimitiveImpl Source #

CCHM primComp is implemented in terms of hcomp and transport. The definition of it comes from mkComp.

primTransHComp :: Command -> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term) Source #

primPartial' :: TCM PrimitiveImpl Source #

primPartialP' :: TCM PrimitiveImpl Source #

primSubOut' :: TCM PrimitiveImpl Source #

primTrans' :: TCM PrimitiveImpl Source #

primHComp' :: TCM PrimitiveImpl Source #

mkComp :: forall m. HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term) 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.

doPiKanOp Source #

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 #

primFaceForall' :: TCM PrimitiveImpl 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 #

tryTranspError :: TCM a -> TCM (Either (Closure (Abs Type)) a) Source #

transpPathPTel' Source #

Arguments

:: NamesT TCM (Abs (Abs Telescope))	j.i.Δ const on φ
-> [NamesT TCM Term]	x : (i : I) → Δ[0,i] const on φ
-> [NamesT TCM Term]	y : (i : I) → Δ[1,i] const on φ
-> NamesT TCM Term	φ
-> [NamesT TCM Term]	p : PathP (λ j → Δ[j,0]) (x 0) (y 0)
-> NamesT TCM [Arg Term]

transpPathTel' Source #

Arguments

:: NamesT TCM (Abs Telescope)	i.Δ const on φ
-> [NamesT TCM Term]	x : (i : I) → Δ[i] const on φ
-> [NamesT TCM Term]	y : (i : I) → Δ[i] const on φ
-> NamesT TCM Term	φ
-> [NamesT TCM Term]	p : Path (Δ[0]) (x 0) (y 0)
-> NamesT TCM [Arg Term]

trFillPathTel' Source #

Arguments

:: NamesT TCM (Abs Telescope)	i.Δ const on φ
-> [NamesT TCM Term]	x : (i : I) → Δ[i] const on φ
-> [NamesT TCM Term]	y : (i : I) → Δ[i] const on φ
-> NamesT TCM Term	φ
-> [NamesT TCM Term]	p : Path (Δ[0]) (x 0) (y 0)
-> NamesT TCM Term	r
-> NamesT TCM [Arg Term]

trFillPathPTel' Source #

Arguments

:: NamesT TCM (Abs (Abs Telescope))	j.i.Δ const on φ
-> [NamesT TCM Term]	x : (i : I) → Δ[0,i] const on φ
-> [NamesT TCM Term]	y : (i : I) → Δ[1,i] const on φ
-> NamesT TCM Term	φ
-> [NamesT TCM Term]	p : Path ( j -> Δ[j,0]) (x 0) (y 0)
-> NamesT TCM Term	r
-> NamesT TCM [Arg Term]

expTelescope :: Type -> Telescope -> Telescope Source #

expS :: Nat -> Substitution Source #

Γ, Δ^I, i : I |- expS |Δ| : Γ, Δ

fromLType :: LType -> Type Source #

lTypeLevel :: LType -> Level Source #

toLType :: MonadReduce m => Type -> m (Maybe LType) Source #

fromCType :: CType -> Type Source #

toCType :: MonadReduce m => Type -> m (Maybe CType) Source #

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 Source #

debugClause :: String -> Clause -> TCM () Source #

module Agda.TypeChecking.Primitive.Cubical.Id

module Agda.TypeChecking.Primitive.Cubical.Base

module Agda.TypeChecking.Primitive.Cubical.Glue

module Agda.TypeChecking.Primitive.Cubical.HCompU