Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Primitive.Cubical

Synopsis

- 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 :: Type -> Type). HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)
- mkCompLazy :: forall (m :: Type -> Type). 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 :: forall (m :: Type -> Type). (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' :: forall (m :: Type -> Type). (PureTCM m, MonadError TCErr m) => Bool -> Abs Telescope -> Term -> Args -> ExceptT (Closure (Abs Type)) m Args
- transpSysTel' :: forall (m :: Type -> Type). (PureTCM m, MonadError TCErr m) => Bool -> Abs Telescope -> [(Term, Abs [Term])] -> Term -> Args -> ExceptT (Closure (Abs Type)) m Args
- type LM (m :: Type -> Type) a = NamesT (ExceptT (Closure (Abs Type)) m) a
- trFillTel' :: forall (m :: Type -> Type). (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 :: (PureTCM m, MonadError TCErr m) => Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
- pathTelescope' :: (PureTCM m, MonadError (Closure Type) m) => Telescope -> [Arg Term] -> [Arg Term] -> m Telescope
- data TranspError = CannotTransp {
  - errorType :: Closure (Abs Type)
  }
- 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
- data LType = LEl Level Term
- data CType
  - = ClosedType Sort QName
  - | LType LType
- fromLType :: LType -> Type
- lTypeLevel :: LType -> Level
- toLType :: MonadReduce m => Type -> m (Maybe LType)
- fromCType :: CType -> Type
- toCType :: MonadReduce m => Type -> m (Maybe CType)
- transpSys :: forall (m :: Type -> Type). (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.Base
- module Agda.TypeChecking.Primitive.Cubical.Glue
- module Agda.TypeChecking.Primitive.Cubical.HCompU

# Documentation

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 :: Type -> Type). 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 :: forall (m :: Type -> Type). 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 :: forall (m :: Type -> Type). (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' :: forall (m :: Type -> Type). (PureTCM m, MonadError TCErr m) => Bool -> Abs Telescope -> Term -> Args -> ExceptT (Closure (Abs Type)) m Args Source #

transpSysTel' :: forall (m :: Type -> Type). (PureTCM m, MonadError TCErr m) => Bool -> Abs Telescope -> [(Term, Abs [Term])] -> Term -> Args -> ExceptT (Closure (Abs Type)) m Args Source #

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

trFillTel' :: forall (m :: Type -> Type). (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 Source #

Arguments

:: (PureTCM m, MonadError TCErr m) |
=> Telescope | Δ
-> [Arg Term] | lhs : Δ
-> [Arg Term] | rhs : Δ
-> m Telescope |

pathTelescope' Source #

Arguments

:: (PureTCM m, MonadError (Closure Type) m) |
=> Telescope | Δ
-> [Arg Term] | lhs : Δ
-> [Arg Term] | rhs : Δ
-> m Telescope |

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 Source # fromException :: SomeException -> Maybe TranspError Source # displayException :: TranspError -> String Source # backtraceDesired :: TranspError -> Bool Source #
Show TranspError Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> TranspError -> ShowS Source # show :: TranspError -> String Source # showList :: [TranspError] -> ShowS 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 |Δ| : Γ, Δ

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 |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical type SubstArg LType = Term

Methods

applySubst :: Substitution' (SubstArg LType) -> LType -> LType Source #

Show LType Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> LType -> ShowS Source # show :: LType -> String Source # showList :: [LType] -> ShowS Source #
Eq LType Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods (==) :: LType -> LType -> Bool Source # (/=) :: LType -> LType -> Bool Source #
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 |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical type SubstArg CType = Term

Methods

applySubst :: Substitution' (SubstArg CType) -> CType -> CType Source #

Show CType Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> CType -> ShowS Source # show :: CType -> String Source # showList :: [CType] -> ShowS Source #
Eq CType Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods (==) :: CType -> CType -> Bool Source # (/=) :: CType -> CType -> Bool Source #
type SubstArg CType Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical type SubstArg CType = Term

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 :: forall (m :: Type -> Type). (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.Base

module Agda.TypeChecking.Primitive.Cubical.Glue

module Agda.TypeChecking.Primitive.Cubical.HCompU